context dependent components;
authorwenzelm
Sun Jul 11 20:35:50 2004 +0200 (2004-07-11 ago)
changeset 15036cab1c1fc1851
parent 15035 8c57751cd43f
child 15037 19b3b0382303
context dependent components;
src/Provers/classical.ML
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/classical.ML	Sun Jul 11 20:35:23 2004 +0200
     1.2 +++ b/src/Provers/classical.ML	Sun Jul 11 20:35:50 2004 +0200
     1.3 @@ -80,6 +80,7 @@
     1.4    val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
     1.5    val claset: unit -> claset
     1.6    val claset_ref: unit -> claset ref
     1.7 +  val local_claset_of   : Proof.context -> claset
     1.8  
     1.9    val fast_tac          : claset -> int -> tactic
    1.10    val slow_tac          : claset -> int -> tactic
    1.11 @@ -136,6 +137,10 @@
    1.12  signature CLASSICAL =
    1.13  sig
    1.14    include BASIC_CLASSICAL
    1.15 +  val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
    1.16 +  val del_context_safe_wrapper: string -> theory -> theory
    1.17 +  val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
    1.18 +  val del_context_unsafe_wrapper: string -> theory -> theory
    1.19    val print_local_claset: Proof.context -> unit
    1.20    val get_local_claset: Proof.context -> claset
    1.21    val put_local_claset: claset -> Proof.context -> Proof.context
    1.22 @@ -256,12 +261,14 @@
    1.23       dup_netpair   = empty_netpair,
    1.24       xtra_netpair  = empty_netpair};
    1.25  
    1.26 -fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
    1.27 +fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
    1.28    let val pretty_thms = map Display.pretty_thm in
    1.29      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
    1.30        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
    1.31        Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
    1.32 -      Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs)]
    1.33 +      Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
    1.34 +      Pretty.strs ("safe wrappers:" :: map #1 swrappers),
    1.35 +      Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
    1.36      |> Pretty.chunks |> Pretty.writeln
    1.37    end;
    1.38  
    1.39 @@ -565,15 +572,17 @@
    1.40  
    1.41  (*Remove a safe wrapper*)
    1.42  fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
    1.43 -    let val (del,rest) = partition (fn (n,_) => n=name) swrappers
    1.44 -    in if null del then (warning ("No such safe wrapper in claset: "^ name);
    1.45 -                         swrappers) else rest end);
    1.46 +  let val swrappers' = filter_out (equal name o #1) swrappers in
    1.47 +    if length swrappers <> length swrappers' then swrappers'
    1.48 +    else (warning ("No such safe wrapper in claset: "^ name); swrappers)
    1.49 +  end);
    1.50  
    1.51  (*Remove an unsafe wrapper*)
    1.52  fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
    1.53 -    let val (del,rest) = partition (fn (n,_) => n=name) uwrappers
    1.54 -    in if null del then (warning ("No such unsafe wrapper in claset: " ^ name);
    1.55 -                         uwrappers) else rest end);
    1.56 +  let val uwrappers' = filter_out (equal name o #1) uwrappers in
    1.57 +    if length uwrappers <> length uwrappers' then uwrappers'
    1.58 +    else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers)
    1.59 +  end);
    1.60  
    1.61  (* compose a safe tactic alternatively before/after safe_step_tac *)
    1.62  fun cs addSbefore  (name,    tac1) =
    1.63 @@ -772,6 +781,36 @@
    1.64  
    1.65  
    1.66  
    1.67 +(** context dependent claset components **)
    1.68 +
    1.69 +datatype context_cs = ContextCS of
    1.70 + {swrappers: (string * (Proof.context -> wrapper)) list,
    1.71 +  uwrappers: (string * (Proof.context -> wrapper)) list};
    1.72 +
    1.73 +fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
    1.74 +  let
    1.75 +    fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
    1.76 +  in
    1.77 +    cs |> fold_rev (add_wrapper (op addSWrapper)) swrappers
    1.78 +    |> fold_rev (add_wrapper (op addWrapper)) uwrappers
    1.79 +  end;
    1.80 +
    1.81 +fun make_context_cs (swrappers, uwrappers) =
    1.82 +  ContextCS {swrappers = swrappers, uwrappers = uwrappers};
    1.83 +
    1.84 +val empty_context_cs = make_context_cs ([], []);
    1.85 +
    1.86 +fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
    1.87 +  let
    1.88 +    val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
    1.89 +    val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
    1.90 +
    1.91 +    val swrappers' = merge_alists swrappers1 swrappers2;
    1.92 +    val uwrappers' = merge_alists uwrappers1 uwrappers2;
    1.93 +  in make_context_cs (swrappers', uwrappers') end;
    1.94 +
    1.95 +
    1.96 +
    1.97  (** claset theory data **)
    1.98  
    1.99  (* theory data kind 'Provers/claset' *)
   1.100 @@ -779,19 +818,24 @@
   1.101  structure GlobalClasetArgs =
   1.102  struct
   1.103    val name = "Provers/claset";
   1.104 -  type T = claset ref;
   1.105 +  type T = claset ref * context_cs;
   1.106  
   1.107 -  val empty = ref empty_cs;
   1.108 -  fun copy (ref cs) = (ref cs): T;            (*create new reference!*)
   1.109 +  val empty = (ref empty_cs, empty_context_cs);
   1.110 +  fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;            (*create new reference!*)
   1.111    val prep_ext = copy;
   1.112 -  fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2));
   1.113 -  fun print _ (ref cs) = print_cs cs;
   1.114 +  fun merge ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
   1.115 +    (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
   1.116 +  fun print _ (ref cs, _) = print_cs cs;
   1.117  end;
   1.118  
   1.119  structure GlobalClaset = TheoryDataFun(GlobalClasetArgs);
   1.120  val print_claset = GlobalClaset.print;
   1.121 -val claset_ref_of_sg = GlobalClaset.get_sg;
   1.122 -val claset_ref_of = GlobalClaset.get;
   1.123 +val claset_ref_of_sg = #1 o GlobalClaset.get_sg;
   1.124 +val claset_ref_of = #1 o GlobalClaset.get;
   1.125 +val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
   1.126 +
   1.127 +fun map_context_cs f = GlobalClaset.map (apsnd
   1.128 +  (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   1.129  
   1.130  
   1.131  (* access claset *)
   1.132 @@ -819,6 +863,15 @@
   1.133  val Delrules = change_claset (op delrules);
   1.134  
   1.135  
   1.136 +(* context dependent components *)
   1.137 +
   1.138 +fun add_context_safe_wrapper wrapper = map_context_cs (apfst (merge_alists [wrapper]));
   1.139 +fun del_context_safe_wrapper name = map_context_cs (apfst (filter_out (equal name o #1)));
   1.140 +
   1.141 +fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd (merge_alists [wrapper]));
   1.142 +fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1)));
   1.143 +
   1.144 +
   1.145  (* proof data kind 'Provers/claset' *)
   1.146  
   1.147  structure LocalClasetArgs =
   1.148 @@ -826,7 +879,7 @@
   1.149    val name = "Provers/claset";
   1.150    type T = claset;
   1.151    val init = claset_of;
   1.152 -  fun print _ cs = print_cs cs;
   1.153 +  fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
   1.154  end;
   1.155  
   1.156  structure LocalClaset = ProofDataFun(LocalClasetArgs);
   1.157 @@ -834,6 +887,9 @@
   1.158  val get_local_claset = LocalClaset.get;
   1.159  val put_local_claset = LocalClaset.put;
   1.160  
   1.161 +fun local_claset_of ctxt =
   1.162 +  context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
   1.163 +
   1.164  
   1.165  (* attributes *)
   1.166  
   1.167 @@ -925,10 +981,10 @@
   1.168  (** proof methods **)
   1.169  
   1.170  fun METHOD_CLASET tac ctxt =
   1.171 -  Method.METHOD (tac ctxt (get_local_claset ctxt));
   1.172 +  Method.METHOD (tac ctxt (local_claset_of ctxt));
   1.173  
   1.174  fun METHOD_CLASET' tac ctxt =
   1.175 -  Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt));
   1.176 +  Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
   1.177  
   1.178  
   1.179  local
   1.180 @@ -974,10 +1030,10 @@
   1.181    Args.del -- Args.colon >> K (I, rule_del_local)];
   1.182  
   1.183  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   1.184 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
   1.185 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
   1.186  
   1.187  fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
   1.188 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
   1.189 +  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
   1.190  
   1.191  val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
   1.192  val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
     2.1 --- a/src/Provers/simplifier.ML	Sun Jul 11 20:35:23 2004 +0200
     2.2 +++ b/src/Provers/simplifier.ML	Sun Jul 11 20:35:50 2004 +0200
     2.3 @@ -9,10 +9,12 @@
     2.4  signature BASIC_SIMPLIFIER =
     2.5  sig
     2.6    include BASIC_META_SIMPLIFIER
     2.7 -  val simproc_i: Sign.sg -> string -> term list
     2.8 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
     2.9 -  val simproc: Sign.sg -> string -> string list
    2.10 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    2.11 +  type context_solver
    2.12 +  val mk_context_solver: string -> (Proof.context -> thm list -> int -> tactic)
    2.13 +    -> context_solver
    2.14 +  type context_simproc
    2.15 +  val mk_context_simproc: string -> cterm list ->
    2.16 +    (Proof.context -> simpset -> term -> thm option) -> context_simproc
    2.17    val print_simpset: theory -> unit
    2.18    val simpset_ref_of_sg: Sign.sg -> simpset ref
    2.19    val simpset_ref_of: theory -> simpset ref
    2.20 @@ -28,6 +30,7 @@
    2.21    val Delsimprocs: simproc list -> unit
    2.22    val Addcongs: thm list -> unit
    2.23    val Delcongs: thm list -> unit
    2.24 +  val local_simpset_of: Proof.context -> simpset
    2.25    val safe_asm_full_simp_tac: simpset -> int -> tactic
    2.26    val               simp_tac: simpset -> int -> tactic
    2.27    val           asm_simp_tac: simpset -> int -> tactic
    2.28 @@ -49,11 +52,28 @@
    2.29  signature SIMPLIFIER =
    2.30  sig
    2.31    include BASIC_SIMPLIFIER
    2.32 +  val simproc_i: Sign.sg -> string -> term list
    2.33 +    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    2.34 +  val simproc: Sign.sg -> string -> string list
    2.35 +    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    2.36 +  val context_simproc_i: Sign.sg -> string -> term list
    2.37 +    -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    2.38 +  val context_simproc: Sign.sg -> string -> string list
    2.39 +    -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    2.40    val          rewrite: simpset -> cterm -> thm
    2.41    val      asm_rewrite: simpset -> cterm -> thm
    2.42    val     full_rewrite: simpset -> cterm -> thm
    2.43    val   asm_lr_rewrite: simpset -> cterm -> thm
    2.44    val asm_full_rewrite: simpset -> cterm -> thm
    2.45 +  val add_context_simprocs: context_simproc list -> theory -> theory
    2.46 +  val del_context_simprocs: context_simproc list -> theory -> theory
    2.47 +  val set_context_subgoaler: (Proof.context -> simpset -> int -> tactic) -> theory -> theory
    2.48 +  val reset_context_subgoaler: theory -> theory
    2.49 +  val add_context_looper: string * (Proof.context -> int -> Tactical.tactic) ->
    2.50 +    theory -> theory
    2.51 +  val del_context_looper: string -> theory -> theory
    2.52 +  val add_context_unsafe_solver: context_solver -> theory -> theory
    2.53 +  val add_context_safe_solver: context_solver -> theory -> theory
    2.54    val print_local_simpset: Proof.context -> unit
    2.55    val get_local_simpset: Proof.context -> simpset
    2.56    val put_local_simpset: simpset -> Proof.context -> Proof.context
    2.57 @@ -81,6 +101,81 @@
    2.58  open MetaSimplifier;
    2.59  
    2.60  
    2.61 +(** context dependent simpset components **)
    2.62 +
    2.63 +(* datatype context_solver *)
    2.64 +
    2.65 +datatype context_solver =
    2.66 +  ContextSolver of (string * (Proof.context -> thm list -> int -> tactic)) * stamp;
    2.67 +
    2.68 +fun mk_context_solver name f = ContextSolver ((name, f), stamp ());
    2.69 +fun eq_context_solver (ContextSolver (_, id1), ContextSolver (_, id2)) = (id1 = id2);
    2.70 +val merge_context_solvers = gen_merge_lists eq_context_solver;
    2.71 +
    2.72 +
    2.73 +(* datatype context_simproc *)
    2.74 +
    2.75 +datatype context_simproc = ContextSimproc of
    2.76 +  (string * cterm list * (Proof.context -> simpset -> term -> thm option)) * stamp;
    2.77 +
    2.78 +fun mk_context_simproc name lhss f = ContextSimproc ((name, lhss, f), stamp ());
    2.79 +fun eq_context_simproc (ContextSimproc (_, id1), ContextSimproc (_, id2)) = (id1 = id2);
    2.80 +val merge_context_simprocs = gen_merge_lists eq_context_simproc;
    2.81 +
    2.82 +fun context_simproc_i sg name =
    2.83 +  mk_context_simproc name o map (Thm.cterm_of sg o Logic.varify);
    2.84 +
    2.85 +fun context_simproc sg name =
    2.86 +  context_simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
    2.87 +
    2.88 +
    2.89 +(* datatype context_ss *)
    2.90 +
    2.91 +datatype context_ss = ContextSS of
    2.92 + {simprocs: context_simproc list,
    2.93 +  subgoal_tac: (Proof.context -> simpset -> int -> tactic) option,
    2.94 +  loop_tacs: (string * (Proof.context -> int -> tactic)) list,
    2.95 +  unsafe_solvers: context_solver list,
    2.96 +  solvers: context_solver list};
    2.97 +
    2.98 +fun context_ss ctxt ss ctxt_ss =
    2.99 +  let
   2.100 +    val ContextSS {simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers} = ctxt_ss;
   2.101 +    fun prep_simproc (ContextSimproc ((name, lhss, f), _)) =
   2.102 +      mk_simproc name lhss (K (f ctxt));
   2.103 +    fun add_loop (name, f) simpset = simpset addloop (name, f ctxt);
   2.104 +    fun add_solver add (ContextSolver ((name, f), _)) simpset =
   2.105 +      add (simpset, mk_solver name (f ctxt));
   2.106 +  in
   2.107 +    ((case subgoal_tac of None => ss | Some tac => ss setsubgoaler tac ctxt)
   2.108 +      addsimprocs map prep_simproc simprocs)
   2.109 +    |> fold_rev add_loop loop_tacs
   2.110 +    |> fold_rev (add_solver (op addSolver)) unsafe_solvers
   2.111 +    |> fold_rev (add_solver (op addSSolver)) solvers
   2.112 +  end;
   2.113 +
   2.114 +fun make_context_ss (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =
   2.115 +  ContextSS {simprocs = simprocs, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
   2.116 +    unsafe_solvers = unsafe_solvers, solvers = solvers};
   2.117 +
   2.118 +val empty_context_ss = make_context_ss ([], None, [], [], []);
   2.119 +
   2.120 +fun merge_context_ss (ctxt_ss1, ctxt_ss2) =
   2.121 +  let
   2.122 +    val ContextSS {simprocs = simprocs1, subgoal_tac = subgoal_tac1, loop_tacs = loop_tacs1,
   2.123 +      unsafe_solvers = unsafe_solvers1, solvers = solvers1} = ctxt_ss1;
   2.124 +    val ContextSS {simprocs = simprocs2, subgoal_tac = subgoal_tac2, loop_tacs = loop_tacs2,
   2.125 +      unsafe_solvers = unsafe_solvers2, solvers = solvers2} = ctxt_ss2;
   2.126 +
   2.127 +    val simprocs' = merge_context_simprocs simprocs1 simprocs2;
   2.128 +    val subgoal_tac' = (case subgoal_tac1 of None => subgoal_tac2 | some => some);
   2.129 +    val loop_tacs' = merge_alists loop_tacs1 loop_tacs2;
   2.130 +    val unsafe_solvers' = merge_context_solvers unsafe_solvers1 unsafe_solvers2;
   2.131 +    val solvers' = merge_context_solvers solvers1 solvers2;
   2.132 +  in make_context_ss (simprocs', subgoal_tac', loop_tacs', unsafe_solvers', solvers') end;
   2.133 +
   2.134 +
   2.135 +
   2.136  (** global and local simpset data **)
   2.137  
   2.138  (* theory data kind 'Provers/simpset' *)
   2.139 @@ -88,19 +183,25 @@
   2.140  structure GlobalSimpsetArgs =
   2.141  struct
   2.142    val name = "Provers/simpset";
   2.143 -  type T = simpset ref;
   2.144 +  type T = simpset ref * context_ss;
   2.145  
   2.146 -  val empty = ref empty_ss;
   2.147 -  fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
   2.148 +  val empty = (ref empty_ss, empty_context_ss);
   2.149 +  fun copy (ref ss, ctxt_ss) = (ref ss, ctxt_ss): T;            (*create new reference!*)
   2.150    val prep_ext = copy;
   2.151 -  fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   2.152 -  fun print _ (ref ss) = print_ss ss;
   2.153 +  fun merge ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
   2.154 +    (ref (merge_ss (ss1, ss2)), merge_context_ss (ctxt_ss1, ctxt_ss2));
   2.155 +  fun print _ (ref ss, _) = print_ss ss;
   2.156  end;
   2.157  
   2.158  structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
   2.159  val print_simpset = GlobalSimpset.print;
   2.160 -val simpset_ref_of_sg = GlobalSimpset.get_sg;
   2.161 -val simpset_ref_of = GlobalSimpset.get;
   2.162 +val simpset_ref_of_sg = #1 o GlobalSimpset.get_sg;
   2.163 +val simpset_ref_of = #1 o GlobalSimpset.get;
   2.164 +val get_context_ss = #2 o GlobalSimpset.get o ProofContext.theory_of;
   2.165 +
   2.166 +fun map_context_ss f = GlobalSimpset.map (apsnd
   2.167 +  (fn ContextSS {simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers} =>
   2.168 +    make_context_ss (f (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers))));
   2.169  
   2.170  
   2.171  (* access global simpset *)
   2.172 @@ -131,6 +232,47 @@
   2.173  val Delcongs = change_simpset (op delcongs);
   2.174  
   2.175  
   2.176 +(* change context dependent components *)
   2.177 +
   2.178 +fun add_context_simprocs procs =
   2.179 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   2.180 +    (merge_context_simprocs procs simprocs, subgoal_tac, loop_tacs,
   2.181 +      unsafe_solvers, solvers));
   2.182 +
   2.183 +fun del_context_simprocs procs =
   2.184 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   2.185 +    (gen_rems eq_context_simproc (simprocs, procs), subgoal_tac, loop_tacs,
   2.186 +      unsafe_solvers, solvers));
   2.187 +
   2.188 +fun set_context_subgoaler tac =
   2.189 +  map_context_ss (fn (simprocs, _, loop_tacs, unsafe_solvers, solvers) =>
   2.190 +    (simprocs, Some tac, loop_tacs, unsafe_solvers, solvers));
   2.191 +
   2.192 +val reset_context_subgoaler =
   2.193 +  map_context_ss (fn (simprocs, _, loop_tacs, unsafe_solvers, solvers) =>
   2.194 +    (simprocs, None, loop_tacs, unsafe_solvers, solvers));
   2.195 +
   2.196 +fun add_context_looper (name, tac) =
   2.197 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   2.198 +    (simprocs, subgoal_tac, merge_alists [(name, tac)] loop_tacs,
   2.199 +      unsafe_solvers, solvers));
   2.200 +
   2.201 +fun del_context_looper name =
   2.202 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   2.203 +    (simprocs, subgoal_tac, filter_out (equal name o #1) loop_tacs,
   2.204 +      unsafe_solvers, solvers));
   2.205 +
   2.206 +fun add_context_unsafe_solver solver =
   2.207 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   2.208 +    (simprocs, subgoal_tac, loop_tacs,
   2.209 +      merge_context_solvers [solver] unsafe_solvers, solvers));
   2.210 +
   2.211 +fun add_context_safe_solver solver =
   2.212 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   2.213 +    (simprocs, subgoal_tac, loop_tacs, unsafe_solvers,
   2.214 +      merge_context_solvers [solver] solvers));
   2.215 +
   2.216 +
   2.217  (* proof data kind 'Provers/simpset' *)
   2.218  
   2.219  structure LocalSimpsetArgs =
   2.220 @@ -138,7 +280,7 @@
   2.221    val name = "Provers/simpset";
   2.222    type T = simpset;
   2.223    val init = simpset_of;
   2.224 -  fun print _ ss = print_ss ss;
   2.225 +  fun print ctxt ss = print_ss (context_ss ctxt ss (get_context_ss ctxt));
   2.226  end;
   2.227  
   2.228  structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
   2.229 @@ -147,6 +289,9 @@
   2.230  val put_local_simpset = LocalSimpset.put;
   2.231  fun map_local_simpset f ctxt = put_local_simpset (f (get_local_simpset ctxt)) ctxt;
   2.232  
   2.233 +fun local_simpset_of ctxt =
   2.234 +  context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);
   2.235 +
   2.236  
   2.237  (* attributes *)
   2.238  
   2.239 @@ -240,7 +385,7 @@
   2.240  
   2.241  val simplified_attr =
   2.242   (simplified_att simpset_of Attrib.global_thmss,
   2.243 -  simplified_att get_local_simpset Attrib.local_thmss);
   2.244 +  simplified_att local_simpset_of Attrib.local_thmss);
   2.245  
   2.246  end;
   2.247  
   2.248 @@ -289,11 +434,11 @@
   2.249  
   2.250  fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
   2.251    ALLGOALS (Method.insert_tac (prems @ facts)) THEN
   2.252 -    (CHANGED_PROP o ALLGOALS o tac) (get_local_simpset ctxt));
   2.253 +    (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
   2.254  
   2.255  fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
   2.256    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   2.257 -      (CHANGED_PROP oo tac) (get_local_simpset ctxt)));
   2.258 +      (CHANGED_PROP oo tac) (local_simpset_of ctxt)));
   2.259  
   2.260  
   2.261  (* setup_methods *)