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