diff -r d78c093aebeb -r aca9a6380c3f Nominal/LFex.thy
--- a/Nominal/LFex.thy	Mon Mar 15 10:07:15 2010 +0100
+++ b/Nominal/LFex.thy	Mon Mar 15 10:36:09 2010 +0100
@@ -5,6 +5,12 @@
 atom_decl name
 atom_decl ident
 
+ML {* val cheat_fv_rsp = ref false *}
+ML {* val cheat_const_rsp = ref false *}
+ML {* val cheat_equivp = ref false *}
+ML {* val cheat_fv_eqvt = ref false *}
+ML {* val cheat_alpha_eqvt = ref false *}
+
 nominal_datatype kind =
     Type
   | KPi "ty" n::"name" k::"kind" bind n in k