--- a/Nominal/Parser.thy	Wed Mar 17 15:13:03 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 17 15:13:31 2010 +0100
@@ -276,14 +276,14 @@
 *}
 
 (* These 2 are critical, we don't know how to do it in term5 *)
-ML {* val cheat_fv_rsp = ref true *}
-ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
+ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
 
-ML {* val cheat_equivp = ref true *}
+ML {* val cheat_equivp = Unsynchronized.ref true *}
 
 (* Fixes for these 2 are known *)
-ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
-ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_fv_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *)
 
 
 ML {*
@@ -520,7 +520,7 @@
 *}
 
 ML {*
-val recursive = ref false
+val recursive = Unsynchronized.ref false
 *}
 
 ML {*