src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML
changeset 32740 9dd0a2f83429
parent 32672 90f3ce5d27ae
child 32950 5d5e123443b3
child 33108 9d9afd478016
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Tue Sep 29 14:59:24 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Tue Sep 29 16:24:36 2009 +0200
@@ -16,7 +16,7 @@
 
 (* Oracle for preprocessing  *)
 
-val (oracle : (string * (cterm -> thm)) option ref) = ref NONE;
+val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
 
 fun the_oracle () =
   case !oracle of