--- a/src/Tools/Code/code_preproc.ML Wed Jan 01 13:24:23 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML Wed Jan 01 14:29:22 2014 +0100
@@ -143,7 +143,8 @@
val resubst = curry (Term.betapplys o swap) all_vars;
in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
-fun lift_ss_conv f ss ct = f (Simplifier.global_context (theory_of_cterm ct) ss) ct;
+fun lift_ss_conv f ss ct = (* FIXME proper context!? *)
+ f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss) ct;
fun preprocess_conv thy =
let