diff -r 49bdb8d475df -r 7c8cd6eae8e2 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -5,11 +5,11 @@
 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 *}
+ML {* val _ = cheat_fv_rsp := false *}
+ML {* val _ = cheat_const_rsp := false *}
+ML {* val _ = cheat_equivp := false *}
+ML {* val _ = cheat_fv_eqvt := false *}
+ML {* val _ = cheat_alpha_eqvt := false *}
 
 nominal_datatype kind =
     Type