diff -r b9caceeec805 -r 9923b2cee778 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 17 18:52:59 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 17 18:53:23 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 {*
@@ -522,7 +522,7 @@
 *}
 
 ML {*
-val recursive = ref false
+val recursive = Unsynchronized.ref false
 *}
 
 ML {*