--- 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