diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v
index 79b13b0..76d23e0 100644
--- a/theories/extraction/UIML_extraction.v
+++ b/theories/extraction/UIML_extraction.v
@@ -41,8 +41,8 @@ Definition isl_A v f := Af v f.
   Notable exception: (a ∨b) → c *)
 Definition isl_simp f := simp_form f.
 
-Definition isl_simplified_E p ψ := E p [ψ].
-Definition isl_simplified_A p ψ := Af p (ψ).
+Definition isl_simplified_E p ψ := Ef p ψ.
+Definition isl_simplified_A p ψ := Af p ψ.
 
 Set Extraction Output Directory "extraction".