1.1 --- a/src/Pure/meta_simplifier.ML	Thu Jan 04 20:01:02 2007 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Jan 04 21:18:05 2007 +0100
     1.3 @@ -45,8 +45,8 @@
     1.4    val empty_ss: simpset
     1.5    val merge_ss: simpset * simpset -> simpset
     1.6    type simproc
     1.7 -  val mk_simproc: string -> cterm list ->
     1.8 -    (theory -> simpset -> term -> thm option) -> simproc
     1.9 +  val mk_simproc': string -> cterm list -> (simpset -> cterm -> thm option) -> simproc
    1.10 +  val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
    1.11    val add_prems: thm list -> simpset -> simpset
    1.12    val prems_of_ss: simpset -> thm list
    1.13    val addsimps: simpset * thm list -> simpset
    1.14 @@ -198,7 +198,7 @@
    1.15    Proc of
    1.16     {name: string,
    1.17      lhs: cterm,
    1.18 -    proc: theory -> simpset -> term -> thm option,
    1.19 +    proc: simpset -> cterm -> thm option,
    1.20      id: stamp}
    1.21  and solver =
    1.22    Solver of
    1.23 @@ -336,23 +336,6 @@
    1.24    end;
    1.25  
    1.26  
    1.27 -(* simprocs *)
    1.28 -
    1.29 -exception SIMPROC_FAIL of string * exn;
    1.30 -
    1.31 -datatype simproc = Simproc of proc list;
    1.32 -
    1.33 -fun mk_simproc name lhss proc =
    1.34 -  let val id = stamp () in
    1.35 -    Simproc (lhss |> map (fn lhs =>
    1.36 -      Proc {name = name, lhs = lhs, proc = proc, id = id}))
    1.37 -  end;
    1.38 -
    1.39 -(* FIXME avoid global thy and Logic.varify *)
    1.40 -fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
    1.41 -fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);
    1.42 -
    1.43 -
    1.44  
    1.45  (** simpset operations **)
    1.46  
    1.47 @@ -377,8 +360,9 @@
    1.48  
    1.49  val theory_context = context o ProofContext.init;
    1.50  
    1.51 -fun fallback_context _ (ss as Simpset ({context = SOME _, ...}, _)) = ss
    1.52 -  | fallback_context thy ss =
    1.53 +fun activate_context thy (ss as Simpset ({context = SOME ctxt, ...}, _)) =
    1.54 +      context (Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt) ss
    1.55 +  | activate_context thy ss =
    1.56       (warning "Simplifier: no proof context in simpset -- fallback to theory context!";
    1.57        theory_context thy ss);
    1.58  
    1.59 @@ -617,6 +601,23 @@
    1.60  
    1.61  (* simprocs *)
    1.62  
    1.63 +exception SIMPROC_FAIL of string * exn;
    1.64 +
    1.65 +datatype simproc = Simproc of proc list;
    1.66 +
    1.67 +fun mk_simproc' name lhss proc =
    1.68 +  let val id = stamp ()
    1.69 +  in Simproc (lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc, id = id})) end;
    1.70 +
    1.71 +fun mk_simproc name lhss proc =
    1.72 +  mk_simproc' name lhss (fn ss => fn ct =>
    1.73 +    proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct));
    1.74 +
    1.75 +(* FIXME avoid global thy and Logic.varify *)
    1.76 +fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
    1.77 +fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);
    1.78 +
    1.79 +
    1.80  local
    1.81  
    1.82  fun add_proc (proc as Proc {name, lhs, ...}) ss =
    1.83 @@ -915,7 +916,7 @@
    1.84            if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
    1.85              (debug_term false ("Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
    1.86               case transform_failure (curry SIMPROC_FAIL name)
    1.87 -                 (fn () => proc thyt ss eta_t) () of
    1.88 +                 (fn () => proc ss eta_t') () of
    1.89                 NONE => (debug false "FAILED"; proc_rews ps)
    1.90               | SOME raw_thm =>
    1.91                   (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") ss raw_thm;
    1.92 @@ -1192,7 +1193,7 @@
    1.93    let
    1.94      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
    1.95      val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
    1.96 -    val ss = fallback_context thy raw_ss;
    1.97 +    val ss = activate_context thy raw_ss;
    1.98      val _ = inc simp_depth;
    1.99      val _ =
   1.100        if ! simp_depth mod 20 = 0 then