clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
authorwenzelm
Thu Dec 12 22:38:25 2013 +0100 (2013-12-12)
changeset 54731384ac33802b0
parent 54730 de2d99b459b3
child 54732 b01bb3d09928
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
src/Pure/Tools/simplifier_trace.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/Tools/simplifier_trace.ML	Thu Dec 12 21:28:13 2013 +0100
     1.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Thu Dec 12 22:38:25 2013 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    Attrib.setup_config_bool @{binding simp_trace_test} (K false)
     1.5  
     1.6  val _ = Theory.setup
     1.7 -  (Simplifier.map_theory_simpset (Simplifier.set_trace_ops
     1.8 +  (Simplifier.set_trace_ops
     1.9     {trace_invoke = fn {depth, term} => fn ctxt =>
    1.10        (if Config.get ctxt simp_trace_test then
    1.11          tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
    1.12 @@ -27,7 +27,7 @@
    1.13      trace_apply = fn args => fn ctxt => fn cont =>
    1.14        (if Config.get ctxt simp_trace_test then
    1.15          tracing ("Simplifier " ^ @{make_string} args)
    1.16 -       else (); cont ctxt)}))
    1.17 +       else (); cont ctxt)})
    1.18  
    1.19  
    1.20  (* PIDE protocol *)
     2.1 --- a/src/Pure/raw_simplifier.ML	Thu Dec 12 21:28:13 2013 +0100
     2.2 +++ b/src/Pure/raw_simplifier.ML	Thu Dec 12 22:38:25 2013 +0100
     2.3 @@ -73,7 +73,7 @@
     2.4    include BASIC_RAW_SIMPLIFIER
     2.5    exception SIMPLIFIER of string * thm
     2.6    type trace_ops
     2.7 -  val set_trace_ops: trace_ops -> Proof.context -> Proof.context
     2.8 +  val set_trace_ops: trace_ops -> theory -> theory
     2.9    val internal_ss: simpset ->
    2.10     {congs: (cong_name * thm) list * cong_name list,
    2.11      procs: proc Net.net,
    2.12 @@ -86,8 +86,7 @@
    2.13      termless: term * term -> bool,
    2.14      subgoal_tac: Proof.context -> int -> tactic,
    2.15      loop_tacs: (string * (Proof.context -> int -> tactic)) list,
    2.16 -    solvers: solver list * solver list,
    2.17 -    trace_ops: trace_ops}
    2.18 +    solvers: solver list * solver list}
    2.19    val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
    2.20    val prems_of: Proof.context -> thm list
    2.21    val add_simp: thm -> Proof.context -> Proof.context
    2.22 @@ -247,18 +246,6 @@
    2.23  fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
    2.24  
    2.25  
    2.26 -(* trace operations *)
    2.27 -
    2.28 -type trace_ops =
    2.29 - {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
    2.30 -  trace_apply: {unconditional: bool, term: term, thm: thm, name: string} ->
    2.31 -    Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
    2.32 -
    2.33 -val no_trace_ops : trace_ops =
    2.34 - {trace_invoke = fn _ => fn ctxt => ctxt,
    2.35 -  trace_apply = fn _ => fn ctxt => fn cont => cont ctxt};
    2.36 -
    2.37 -
    2.38  (* simplification sets *)
    2.39  
    2.40  (*A simpset contains data required during conversion:
    2.41 @@ -296,8 +283,7 @@
    2.42      termless: term * term -> bool,
    2.43      subgoal_tac: Proof.context -> int -> tactic,
    2.44      loop_tacs: (string * (Proof.context -> int -> tactic)) list,
    2.45 -    solvers: solver list * solver list,
    2.46 -    trace_ops: trace_ops};
    2.47 +    solvers: solver list * solver list};
    2.48  
    2.49  fun internal_ss (Simpset (_, ss2)) = ss2;
    2.50  
    2.51 @@ -307,12 +293,12 @@
    2.52  fun map_ss1 f {rules, prems, bounds, depth} =
    2.53    make_ss1 (f (rules, prems, bounds, depth));
    2.54  
    2.55 -fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =
    2.56 +fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
    2.57    {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
    2.58 -    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers, trace_ops = trace_ops};
    2.59 +    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
    2.60  
    2.61 -fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops} =
    2.62 -  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
    2.63 +fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
    2.64 +  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
    2.65  
    2.66  fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
    2.67  
    2.68 @@ -332,9 +318,9 @@
    2.69  
    2.70  (* empty *)
    2.71  
    2.72 -fun init_ss mk_rews termless subgoal_tac solvers trace_ops =
    2.73 +fun init_ss mk_rews termless subgoal_tac solvers =
    2.74    make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false)),
    2.75 -    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers, trace_ops));
    2.76 +    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
    2.77  
    2.78  fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
    2.79  
    2.80 @@ -345,9 +331,7 @@
    2.81        mk_sym = default_mk_sym,
    2.82        mk_eq_True = K (K NONE),
    2.83        reorient = default_reorient}
    2.84 -    Term_Ord.termless (K (K no_tac))
    2.85 -    ([], [])
    2.86 -    no_trace_ops;
    2.87 +    Term_Ord.termless (K (K no_tac)) ([], []);
    2.88  
    2.89  
    2.90  (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
    2.91 @@ -358,10 +342,10 @@
    2.92      let
    2.93        val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1},
    2.94         {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
    2.95 -        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1), trace_ops}) = ss1;
    2.96 +        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
    2.97        val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2},
    2.98         {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
    2.99 -        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2), trace_ops = _}) = ss2;
   2.100 +        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   2.101  
   2.102        val rules' = Net.merge eq_rrule (rules1, rules2);
   2.103        val prems' = Thm.merge_thms (prems1, prems2);
   2.104 @@ -375,7 +359,7 @@
   2.105        val solvers' = merge eq_solver (solvers1, solvers2);
   2.106      in
   2.107        make_simpset ((rules', prems', bounds', depth'), ((congs', weak'), procs',
   2.108 -        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'), trace_ops))
   2.109 +        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
   2.110      end;
   2.111  
   2.112  
   2.113 @@ -400,13 +384,9 @@
   2.114  
   2.115  fun put_simpset ss = map_simpset (fn context_ss =>
   2.116    let
   2.117 -    val Simpset ({rules, prems, ...},  (* FIXME prems from context (!?) *)
   2.118 -      {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, ...}) = ss;
   2.119 -    val Simpset ({bounds, depth, ...}, {trace_ops, ...}) = context_ss;
   2.120 -  in
   2.121 -    Simpset (make_ss1 (rules, prems, bounds, depth),
   2.122 -      make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops))
   2.123 -  end);
   2.124 +    val Simpset ({rules, prems, ...}, ss2) = ss;  (* FIXME prems from context (!?) *)
   2.125 +    val Simpset ({bounds, depth, ...}, _) = context_ss;
   2.126 +  in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end);
   2.127  
   2.128  fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss;
   2.129  
   2.130 @@ -421,8 +401,8 @@
   2.131  fun map_ss f = Context.mapping (map_theory_simpset f) f;
   2.132  
   2.133  val clear_simpset =
   2.134 -  map_simpset (fn Simpset (_, {mk_rews, termless, subgoal_tac, solvers, trace_ops, ...}) =>
   2.135 -    init_ss mk_rews termless subgoal_tac solvers trace_ops);
   2.136 +  map_simpset (fn Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
   2.137 +    init_ss mk_rews termless subgoal_tac solvers);
   2.138  
   2.139  
   2.140  (* simp depth *)
   2.141 @@ -686,7 +666,7 @@
   2.142  in
   2.143  
   2.144  fun add_eqcong thm ctxt = ctxt |> map_simpset2
   2.145 -  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.146 +  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   2.147      let
   2.148        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
   2.149          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   2.150 @@ -701,10 +681,10 @@
   2.151          else ();
   2.152        val xs' = AList.update (op =) (a, thm) xs;
   2.153        val weak' = if is_full_cong thm then weak else a :: weak;
   2.154 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) end);
   2.155 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   2.156  
   2.157  fun del_eqcong thm ctxt = ctxt |> map_simpset2
   2.158 -  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.159 +  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   2.160      let
   2.161        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
   2.162          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   2.163 @@ -715,7 +695,7 @@
   2.164        val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
   2.165        val weak' = xs' |> map_filter (fn (a, thm) =>
   2.166          if is_full_cong thm then NONE else SOME a);
   2.167 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) end);
   2.168 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   2.169  
   2.170  fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt;
   2.171  fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt;
   2.172 @@ -758,18 +738,18 @@
   2.173  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
   2.174   (trace_cterm ctxt false (fn () => "Adding simplification procedure " ^ quote name ^ " for") lhs;
   2.175    ctxt |> map_simpset2
   2.176 -    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.177 +    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   2.178        (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
   2.179 -        mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops))
   2.180 +        mk_rews, termless, subgoal_tac, loop_tacs, solvers))
   2.181    handle Net.INSERT =>
   2.182      (Context_Position.if_visible ctxt
   2.183        warning ("Ignoring duplicate simplification procedure " ^ quote name); ctxt));
   2.184  
   2.185  fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
   2.186    ctxt |> map_simpset2
   2.187 -    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.188 +    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   2.189        (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
   2.190 -        mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops))
   2.191 +        mk_rews, termless, subgoal_tac, loop_tacs, solvers))
   2.192    handle Net.DELETE =>
   2.193      (Context_Position.if_visible ctxt
   2.194        warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ctxt);
   2.195 @@ -790,14 +770,14 @@
   2.196  local
   2.197  
   2.198  fun map_mk_rews f =
   2.199 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.200 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   2.201      let
   2.202        val {mk, mk_cong, mk_sym, mk_eq_True, reorient} = mk_rews;
   2.203        val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
   2.204          f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
   2.205        val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
   2.206          reorient = reorient'};
   2.207 -    in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers, trace_ops) end);
   2.208 +    in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
   2.209  
   2.210  in
   2.211  
   2.212 @@ -826,62 +806,75 @@
   2.213  (* termless *)
   2.214  
   2.215  fun set_termless termless =
   2.216 -  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.217 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
   2.218 +  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
   2.219 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   2.220  
   2.221  
   2.222  (* tactics *)
   2.223  
   2.224  fun set_subgoaler subgoal_tac =
   2.225 -  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers, trace_ops) =>
   2.226 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
   2.227 +  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
   2.228 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   2.229  
   2.230  fun ctxt setloop tac = ctxt |>
   2.231 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers, trace_ops) =>
   2.232 -   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers, trace_ops));
   2.233 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
   2.234 +   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
   2.235  
   2.236  fun ctxt addloop (name, tac) = ctxt |>
   2.237 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.238 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   2.239      (congs, procs, mk_rews, termless, subgoal_tac,
   2.240 -     AList.update (op =) (name, tac) loop_tacs, solvers, trace_ops));
   2.241 +     AList.update (op =) (name, tac) loop_tacs, solvers));
   2.242  
   2.243  fun ctxt delloop name = ctxt |>
   2.244 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) =>
   2.245 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   2.246      (congs, procs, mk_rews, termless, subgoal_tac,
   2.247       (if AList.defined (op =) loop_tacs name then ()
   2.248        else
   2.249          Context_Position.if_visible ctxt
   2.250            warning ("No such looper in simpset: " ^ quote name);
   2.251 -        AList.delete (op =) name loop_tacs), solvers, trace_ops));
   2.252 +        AList.delete (op =) name loop_tacs), solvers));
   2.253  
   2.254  fun ctxt setSSolver solver = ctxt |> map_simpset2
   2.255 -  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _), trace_ops) =>
   2.256 -    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]), trace_ops));
   2.257 +  (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
   2.258 +    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
   2.259  
   2.260  fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   2.261 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers), trace_ops) => (congs, procs, mk_rews, termless,
   2.262 -    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers), trace_ops));
   2.263 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   2.264 +    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
   2.265  
   2.266  fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   2.267 -  subgoal_tac, loop_tacs, (_, solvers), trace_ops) => (congs, procs, mk_rews, termless,
   2.268 -    subgoal_tac, loop_tacs, ([solver], solvers), trace_ops));
   2.269 +  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
   2.270 +    subgoal_tac, loop_tacs, ([solver], solvers)));
   2.271  
   2.272  fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   2.273 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers), trace_ops) => (congs, procs, mk_rews, termless,
   2.274 -    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers), trace_ops));
   2.275 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   2.276 +    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
   2.277  
   2.278  fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
   2.279 -  subgoal_tac, loop_tacs, _, trace_ops) => (congs, procs, mk_rews, termless,
   2.280 -  subgoal_tac, loop_tacs, (solvers, solvers), trace_ops));
   2.281 +  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
   2.282 +  subgoal_tac, loop_tacs, (solvers, solvers)));
   2.283  
   2.284  
   2.285  (* trace operations *)
   2.286  
   2.287 -fun set_trace_ops trace_ops =
   2.288 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, _) =>
   2.289 -    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops));
   2.290 +type trace_ops =
   2.291 + {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
   2.292 +  trace_apply: {unconditional: bool, term: term, thm: thm, name: string} ->
   2.293 +    Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
   2.294  
   2.295 -val trace_ops = #trace_ops o internal_ss o simpset_of;
   2.296 +structure Trace_Ops = Theory_Data
   2.297 +(
   2.298 +  type T = trace_ops;
   2.299 +  val empty: T =
   2.300 +   {trace_invoke = fn _ => fn ctxt => ctxt,
   2.301 +    trace_apply = fn _ => fn ctxt => fn cont => cont ctxt};
   2.302 +  val extend = I;
   2.303 +  fun merge (trace_ops, _) = trace_ops;
   2.304 +);
   2.305 +
   2.306 +val set_trace_ops = Trace_Ops.put;
   2.307 +
   2.308 +val trace_ops = Trace_Ops.get o Proof_Context.theory_of;
   2.309  fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt;
   2.310  fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt;
   2.311  
     3.1 --- a/src/Pure/simplifier.ML	Thu Dec 12 21:28:13 2013 +0100
     3.2 +++ b/src/Pure/simplifier.ML	Thu Dec 12 22:38:25 2013 +0100
     3.3 @@ -48,7 +48,7 @@
     3.4    val set_termless: (term * term -> bool) -> Proof.context -> Proof.context
     3.5    val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
     3.6    type trace_ops
     3.7 -  val set_trace_ops: trace_ops -> Proof.context -> Proof.context
     3.8 +  val set_trace_ops: trace_ops -> theory -> theory
     3.9    val simproc_global_i: theory -> string -> term list ->
    3.10      (Proof.context -> term -> thm option) -> simproc
    3.11    val simproc_global: theory -> string -> string list ->