--- a/src/Tools/Code/code_preproc.ML Fri Sep 06 15:47:51 2013 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Sep 06 20:55:14 2013 +0200
@@ -143,7 +143,7 @@
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.put_simpset ss (Proof_Context.init_global (theory_of_cterm ct))) ct;
+fun lift_ss_conv f ss ct = f (Simplifier.global_context (theory_of_cterm ct) ss) ct;
fun preprocess_conv thy =
let