1.1 --- a/src/Tools/Code/code_preproc.ML	Fri Jan 03 21:52:00 2014 +0100
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Fri Jan 03 22:04:44 2014 +0100
     1.3 @@ -143,14 +143,15 @@
     1.4      val resubst = curry (Term.betapplys o swap) all_vars;
     1.5    in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
     1.6  
     1.7 -fun lift_ss_conv f ss ct =  (* FIXME proper context!? *)
     1.8 -  f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss) ct;
     1.9 +fun global_simpset_context thy ss =
    1.10 +  Proof_Context.init_global thy
    1.11 +  |> put_simpset ss;
    1.12  
    1.13  fun preprocess_conv thy =
    1.14    let
    1.15 -    val pre = (#pre o the_thmproc) thy;
    1.16 +    val pre = global_simpset_context thy ((#pre o the_thmproc) thy);
    1.17    in
    1.18 -    lift_ss_conv Simplifier.rewrite pre
    1.19 +    Simplifier.rewrite pre
    1.20      #> trans_conv_rule (Axclass.unoverload_conv thy)
    1.21    end;
    1.22  
    1.23 @@ -158,10 +159,10 @@
    1.24  
    1.25  fun postprocess_conv thy =
    1.26    let
    1.27 -    val post = (#post o the_thmproc) thy;
    1.28 +    val post = global_simpset_context thy ((#post o the_thmproc) thy);
    1.29    in
    1.30      Axclass.overload_conv thy
    1.31 -    #> trans_conv_rule (lift_ss_conv Simplifier.rewrite post)
    1.32 +    #> trans_conv_rule (Simplifier.rewrite post)
    1.33    end;
    1.34  
    1.35  fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);

     2.1 --- a/src/Tools/Code/code_simp.ML	Fri Jan 03 21:52:00 2014 +0100
     2.2 +++ b/src/Tools/Code/code_simp.ML	Fri Jan 03 22:04:44 2014 +0100
     2.3 @@ -31,7 +31,11 @@
     2.4  
     2.5  fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
     2.6  
     2.7 -fun simpset_default thy = the_default (Simpset.get thy);
     2.8 +fun simpset_default thy some_ss = the_default (Simpset.get thy) some_ss;
     2.9 +
    2.10 +fun simp_ctxt_default thy some_ss =
    2.11 +  Proof_Context.init_global thy
    2.12 +  |> put_simpset (simpset_default thy some_ss);
    2.13  
    2.14  
    2.15  (* diagnostic *)
    2.16 @@ -59,19 +63,15 @@
    2.17  
    2.18  val add_program = Graph.fold (add_stmt o fst o snd);
    2.19  
    2.20 -fun simpset_program thy some_ss program =
    2.21 -  simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss);
    2.22 -
    2.23 -fun lift_ss_conv f ss ct =  (* FIXME proper context!? *)
    2.24 -  f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss |> set_trace) ct;
    2.25 +fun simp_ctxt_program thy some_ss program =
    2.26 +  simp_ctxt_default thy some_ss
    2.27 +  |> add_program program;
    2.28  
    2.29  fun rewrite_modulo thy some_ss program =
    2.30 -  lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);
    2.31 +  Simplifier.full_rewrite (simp_ctxt_program thy some_ss program |> set_trace);
    2.32  
    2.33  fun conclude_tac thy some_ss =
    2.34 -  let
    2.35 -    val ss = simpset_default thy some_ss;
    2.36 -  in fn ctxt => Simplifier.full_simp_tac (Simplifier.put_simpset ss ctxt) end;
    2.37 +  Simplifier.full_simp_tac o Simplifier.put_simpset (simpset_default thy some_ss);
    2.38  
    2.39  
    2.40  (* evaluation with dynamic code context *)