src/Pure/raw_simplifier.ML
changeset 54729 c5cd7a58cf2d
parent 54728 445e7947c6b5
child 54731 384ac33802b0
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu Dec 12 17:34:50 2013 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Dec 12 21:14:33 2013 +0100
     1.3 @@ -72,6 +72,8 @@
     1.4  sig
     1.5    include BASIC_RAW_SIMPLIFIER
     1.6    exception SIMPLIFIER of string * thm
     1.7 +  type trace_ops
     1.8 +  val set_trace_ops: trace_ops -> Proof.context -> Proof.context
     1.9    val internal_ss: simpset ->
    1.10     {congs: (cong_name * thm) list * cong_name list,
    1.11      procs: proc Net.net,
    1.12 @@ -84,7 +86,8 @@
    1.13      termless: term * term -> bool,
    1.14      subgoal_tac: Proof.context -> int -> tactic,
    1.15      loop_tacs: (string * (Proof.context -> int -> tactic)) list,
    1.16 -    solvers: solver list * solver list}
    1.17 +    solvers: solver list * solver list,
    1.18 +    trace_ops: trace_ops}
    1.19    val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
    1.20    val prems_of: Proof.context -> thm list
    1.21    val add_simp: thm -> Proof.context -> Proof.context
    1.22 @@ -244,6 +247,18 @@
    1.23  fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
    1.24  
    1.25  
    1.26 +(* trace operations *)
    1.27 +
    1.28 +type trace_ops =
    1.29 + {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
    1.30 +  trace_apply: {unconditional: bool, term: term, thm: thm, name: string} ->
    1.31 +    Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
    1.32 +
    1.33 +val no_trace_ops : trace_ops =
    1.34 + {trace_invoke = fn _ => fn ctxt => ctxt,
    1.35 +  trace_apply = fn _ => fn ctxt => fn cont => cont ctxt};
    1.36 +
    1.37 +
    1.38  (* simplification sets *)
    1.39  
    1.40  (*A simpset contains data required during conversion:
    1.41 @@ -281,7 +296,8 @@
    1.42      termless: term * term -> bool,
    1.43      subgoal_tac: Proof.context -> int -> tactic,
    1.44      loop_tacs: (string * (Proof.context -> int -> tactic)) list,
    1.45 -    solvers: solver list * solver list};
    1.46 +    solvers: solver list * solver list,
    1.47 +    trace_ops: trace_ops};
    1.48  
    1.49  fun internal_ss (Simpset (_, ss2)) = ss2;
    1.50  
    1.51 @@ -291,12 +307,12 @@
    1.52  fun map_ss1 f {rules, prems, bounds, depth} =
    1.53    make_ss1 (f (rules, prems, bounds, depth));
    1.54  
    1.55 -fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
    1.56 +fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =
    1.57    {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
    1.58 -    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
    1.59 +    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers, trace_ops = trace_ops};
    1.60  
    1.61 -fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
    1.62 -  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
    1.63 +fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops} =
    1.64 +  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
    1.65  
    1.66  fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
    1.67  
    1.68 @@ -316,9 +332,9 @@
    1.69  
    1.70  (* empty *)
    1.71  
    1.72 -fun init_ss mk_rews termless subgoal_tac solvers =
    1.73 +fun init_ss mk_rews termless subgoal_tac solvers trace_ops =
    1.74    make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false)),
    1.75 -    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
    1.76 +    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers, trace_ops));
    1.77  
    1.78  fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
    1.79  
    1.80 @@ -329,7 +345,9 @@
    1.81        mk_sym = default_mk_sym,
    1.82        mk_eq_True = K (K NONE),
    1.83        reorient = default_reorient}
    1.84 -    Term_Ord.termless (K (K no_tac)) ([], []);
    1.85 +    Term_Ord.termless (K (K no_tac))
    1.86 +    ([], [])
    1.87 +    no_trace_ops;
    1.88  
    1.89  
    1.90  (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
    1.91 @@ -340,10 +358,10 @@
    1.92      let
    1.93        val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1},
    1.94         {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
    1.95 -        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
    1.96 +        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1), trace_ops}) = ss1;
    1.97        val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2},
    1.98         {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
    1.99 -        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   1.100 +        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2), trace_ops = _}) = ss2;
   1.101  
   1.102        val rules' = Net.merge eq_rrule (rules1, rules2);
   1.103        val prems' = Thm.merge_thms (prems1, prems2);
   1.104 @@ -357,7 +375,7 @@
   1.105        val solvers' = merge eq_solver (solvers1, solvers2);
   1.106      in
   1.107        make_simpset ((rules', prems', bounds', depth'), ((congs', weak'), procs',
   1.108 -        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
   1.109 +        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'), trace_ops))
   1.110      end;
   1.111  
   1.112  
   1.113 @@ -380,9 +398,15 @@
   1.114  
   1.115  fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get;
   1.116  
   1.117 -fun put_simpset (Simpset ({rules, prems, ...}, ss2)) =  (* FIXME prems from context (!?) *)
   1.118 -  map_simpset (fn Simpset ({bounds, depth, ...}, _) =>
   1.119 -    Simpset (make_ss1 (rules, prems, bounds, depth), ss2));
   1.120 +fun put_simpset ss = map_simpset (fn context_ss =>
   1.121 +  let
   1.122 +    val Simpset ({rules, prems, ...},  (* FIXME prems from context (!?) *)
   1.123 +      {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, ...}) = ss;
   1.124 +    val Simpset ({bounds, depth, ...}, {trace_ops, ...}) = context_ss;
   1.125 +  in
   1.126 +    Simpset (make_ss1 (rules, prems, bounds, depth),
   1.127 +      make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops))
   1.128 +  end);
   1.129  
   1.130  fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss;
   1.131  
   1.132 @@ -397,8 +421,8 @@
   1.133  fun map_ss f = Context.mapping (map_theory_simpset f) f;
   1.134  
   1.135  val clear_simpset =
   1.136 -  map_simpset (fn Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
   1.137 -    init_ss mk_rews termless subgoal_tac solvers);
   1.138 +  map_simpset (fn Simpset (_, {mk_rews, termless, subgoal_tac, solvers, trace_ops, ...}) =>
   1.139 +    init_ss mk_rews termless subgoal_tac solvers trace_ops);
   1.140  
   1.141  
   1.142  (* simp depth *)
   1.143 @@ -661,8 +685,8 @@
   1.144  
   1.145  in
   1.146  
   1.147 -fun add_eqcong thm ctxt = ctxt |>
   1.148 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.149 +fun add_eqcong thm ctxt = ctxt |> map_simpset2
   1.150 +  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.151      let
   1.152        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
   1.153          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.154 @@ -677,10 +701,10 @@
   1.155          else ();
   1.156        val xs' = AList.update (op =) (a, thm) xs;
   1.157        val weak' = if is_full_cong thm then weak else a :: weak;
   1.158 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   1.159 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) end);
   1.160  
   1.161 -fun del_eqcong thm ctxt = ctxt |>
   1.162 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.163 +fun del_eqcong thm ctxt = ctxt |> map_simpset2
   1.164 +  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.165      let
   1.166        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
   1.167          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.168 @@ -691,7 +715,7 @@
   1.169        val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
   1.170        val weak' = xs' |> map_filter (fn (a, thm) =>
   1.171          if is_full_cong thm then NONE else SOME a);
   1.172 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   1.173 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) end);
   1.174  
   1.175  fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt;
   1.176  fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt;
   1.177 @@ -733,17 +757,19 @@
   1.178  
   1.179  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
   1.180   (trace_cterm ctxt false (fn () => "Adding simplification procedure " ^ quote name ^ " for") lhs;
   1.181 -  ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.182 -    (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
   1.183 -      mk_rews, termless, subgoal_tac, loop_tacs, solvers))
   1.184 +  ctxt |> map_simpset2
   1.185 +    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.186 +      (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
   1.187 +        mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops))
   1.188    handle Net.INSERT =>
   1.189      (Context_Position.if_visible ctxt
   1.190        warning ("Ignoring duplicate simplification procedure " ^ quote name); ctxt));
   1.191  
   1.192  fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
   1.193 -  ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.194 -    (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
   1.195 -      mk_rews, termless, subgoal_tac, loop_tacs, solvers))
   1.196 +  ctxt |> map_simpset2
   1.197 +    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.198 +      (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
   1.199 +        mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops))
   1.200    handle Net.DELETE =>
   1.201      (Context_Position.if_visible ctxt
   1.202        warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ctxt);
   1.203 @@ -763,14 +789,15 @@
   1.204  
   1.205  local
   1.206  
   1.207 -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
   1.208 -      termless, subgoal_tac, loop_tacs, solvers) =>
   1.209 -  let
   1.210 -    val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
   1.211 -      f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
   1.212 -    val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
   1.213 -      reorient = reorient'};
   1.214 -  in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
   1.215 +fun map_mk_rews f =
   1.216 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.217 +    let
   1.218 +      val {mk, mk_cong, mk_sym, mk_eq_True, reorient} = mk_rews;
   1.219 +      val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
   1.220 +        f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
   1.221 +      val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
   1.222 +        reorient = reorient'};
   1.223 +    in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers, trace_ops) end);
   1.224  
   1.225  in
   1.226  
   1.227 @@ -799,53 +826,64 @@
   1.228  (* termless *)
   1.229  
   1.230  fun set_termless termless =
   1.231 -  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
   1.232 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   1.233 +  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.234 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
   1.235  
   1.236  
   1.237  (* tactics *)
   1.238  
   1.239  fun set_subgoaler subgoal_tac =
   1.240 -  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
   1.241 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   1.242 +  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers, trace_ops) =>
   1.243 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
   1.244  
   1.245  fun ctxt setloop tac = ctxt |>
   1.246 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
   1.247 -   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
   1.248 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers, trace_ops) =>
   1.249 +   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers, trace_ops));
   1.250  
   1.251  fun ctxt addloop (name, tac) = ctxt |>
   1.252 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.253 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.254      (congs, procs, mk_rews, termless, subgoal_tac,
   1.255 -     AList.update (op =) (name, tac) loop_tacs, solvers));
   1.256 +     AList.update (op =) (name, tac) loop_tacs, solvers, trace_ops));
   1.257  
   1.258  fun ctxt delloop name = ctxt |>
   1.259 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.260 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   1.261      (congs, procs, mk_rews, termless, subgoal_tac,
   1.262       (if AList.defined (op =) loop_tacs name then ()
   1.263        else
   1.264          Context_Position.if_visible ctxt
   1.265            warning ("No such looper in simpset: " ^ quote name);
   1.266 -        AList.delete (op =) name loop_tacs), solvers));
   1.267 +        AList.delete (op =) name loop_tacs), solvers, trace_ops));
   1.268  
   1.269 -fun ctxt setSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   1.270 -  subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
   1.271 -    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
   1.272 +fun ctxt setSSolver solver = ctxt |> map_simpset2
   1.273 +  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _), trace_ops) =>
   1.274 +    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]), trace_ops));
   1.275  
   1.276  fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   1.277 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   1.278 -    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
   1.279 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers), trace_ops) => (congs, procs, mk_rews, termless,
   1.280 +    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers), trace_ops));
   1.281  
   1.282  fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   1.283 -  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
   1.284 -    subgoal_tac, loop_tacs, ([solver], solvers)));
   1.285 +  subgoal_tac, loop_tacs, (_, solvers), trace_ops) => (congs, procs, mk_rews, termless,
   1.286 +    subgoal_tac, loop_tacs, ([solver], solvers), trace_ops));
   1.287  
   1.288  fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   1.289 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   1.290 -    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
   1.291 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers), trace_ops) => (congs, procs, mk_rews, termless,
   1.292 +    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers), trace_ops));
   1.293  
   1.294  fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
   1.295 -  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
   1.296 -  subgoal_tac, loop_tacs, (solvers, solvers)));
   1.297 +  subgoal_tac, loop_tacs, _, trace_ops) => (congs, procs, mk_rews, termless,
   1.298 +  subgoal_tac, loop_tacs, (solvers, solvers), trace_ops));
   1.299 +
   1.300 +
   1.301 +(* trace operations *)
   1.302 +
   1.303 +fun set_trace_ops trace_ops =
   1.304 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, _) =>
   1.305 +    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
   1.306 +
   1.307 +val trace_ops = #trace_ops o internal_ss o simpset_of;
   1.308 +fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt;
   1.309 +fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt;
   1.310  
   1.311  
   1.312  
   1.313 @@ -943,6 +981,7 @@
   1.314          val prop' = Thm.prop_of thm';
   1.315          val unconditional = (Logic.count_prems prop' = 0);
   1.316          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
   1.317 +        val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', name = name};
   1.318        in
   1.319          if perm andalso not (termless (rhs', lhs'))
   1.320          then
   1.321 @@ -954,10 +993,11 @@
   1.322            if unconditional
   1.323            then
   1.324             (trace_thm ctxt (fn () => "Rewriting:") thm';
   1.325 -            let
   1.326 -              val lr = Logic.dest_equals prop;
   1.327 -              val SOME thm'' = check_conv ctxt false eta_thm thm';
   1.328 -            in SOME (thm'', uncond_skel (congs, lr)) end)
   1.329 +            trace_apply trace_args ctxt (fn ctxt' =>
   1.330 +              let
   1.331 +                val lr = Logic.dest_equals prop;
   1.332 +                val SOME thm'' = check_conv ctxt' false eta_thm thm';
   1.333 +              in SOME (thm'', uncond_skel (congs, lr)) end))
   1.334            else
   1.335             (trace_thm ctxt (fn () => "Trying to rewrite:") thm';
   1.336              if simp_depth ctxt > Config.get ctxt simp_depth_limit
   1.337 @@ -968,16 +1008,17 @@
   1.338                  val _ = Context_Position.if_visible ctxt warning s;
   1.339                in NONE end
   1.340              else
   1.341 -              (case prover ctxt thm' of
   1.342 -                NONE => (trace_thm ctxt (fn () => "FAILED") thm'; NONE)
   1.343 -              | SOME thm2 =>
   1.344 -                  (case check_conv ctxt true eta_thm thm2 of
   1.345 -                    NONE => NONE
   1.346 -                  | SOME thm2' =>
   1.347 -                      let
   1.348 -                        val concl = Logic.strip_imp_concl prop;
   1.349 -                        val lr = Logic.dest_equals concl;
   1.350 -                      in SOME (thm2', cond_skel (congs, lr)) end))))
   1.351 +              trace_apply trace_args ctxt (fn ctxt' =>
   1.352 +                (case prover ctxt' thm' of
   1.353 +                  NONE => (trace_thm ctxt' (fn () => "FAILED") thm'; NONE)
   1.354 +                | SOME thm2 =>
   1.355 +                    (case check_conv ctxt' true eta_thm thm2 of
   1.356 +                      NONE => NONE
   1.357 +                    | SOME thm2' =>
   1.358 +                        let
   1.359 +                          val concl = Logic.strip_imp_concl prop;
   1.360 +                          val lr = Logic.dest_equals concl;
   1.361 +                        in SOME (thm2', cond_skel (congs, lr)) end)))))
   1.362        end;
   1.363  
   1.364      fun rews [] = NONE
   1.365 @@ -1311,11 +1352,7 @@
   1.366  
   1.367  fun rewrite_cterm mode prover raw_ctxt raw_ct =
   1.368    let
   1.369 -    val ctxt =
   1.370 -      raw_ctxt
   1.371 -      |> Context_Position.set_visible false
   1.372 -      |> inc_simp_depth;
   1.373 -    val thy = Proof_Context.theory_of ctxt;
   1.374 +    val thy = Proof_Context.theory_of raw_ctxt;
   1.375  
   1.376      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
   1.377      val {maxidx, ...} = Thm.rep_cterm ct;
   1.378 @@ -1323,6 +1360,12 @@
   1.379        Theory.subthy (theory_of_cterm ct, thy) orelse
   1.380          raise CTERM ("rewrite_cterm: bad background theory", [ct]);
   1.381  
   1.382 +    val ctxt =
   1.383 +      raw_ctxt
   1.384 +      |> Context_Position.set_visible false
   1.385 +      |> inc_simp_depth
   1.386 +      |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
   1.387 +
   1.388      val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
   1.389      val _ = check_bounds ctxt ct;
   1.390    in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;