Fix a broken proof (in an unused file)

CakeML · Oct 7, 2023 · da03bc7 · da03bc7
1 parent 05de3cc
commit da03bc7
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/compiler/backend/languages/properties/env_cexp_lemmasScript.sml b/compiler/backend/languages/properties/env_cexp_lemmasScript.sml
@@ -7,6 +7,8 @@ open pure_miscTheory env_cexpTheory ;
 val _ = new_theory "env_cexp_lemmas";
 
 val freevars_def = envLangTheory.freevars_def;
+val Lams_def = envLangTheory.Lams_def;
+val Apps_def = envLangTheory.Apps_def;
 
 Theorem freevars_Lams[simp]:
   ∀vs e. freevars (Lams vs e) = freevars e DIFF set vs
@@ -106,4 +108,3 @@ QED
  *)
 
 val _ = export_theory();
-