# HG changeset patch
# User haftmann
# Date 1575537874 0
# Node ID d12c58e12c51863ae0001ab5d668c83cea0ef132
# Parent  f1838cf9f13947a8da7a10bf162af0e576d0096c
more direct accessors for simpset

diff -r f1838cf9f139 -r d12c58e12c51 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Dec 04 20:25:21 2019 +0000
+++ b/src/Pure/raw_simplifier.ML	Thu Dec 05 09:24:34 2019 +0000
@@ -73,19 +73,9 @@
   exception SIMPLIFIER of string * thm list
   type trace_ops
   val set_trace_ops: trace_ops -> theory -> theory
-  val internal_ss: simpset ->
-   {congs: (cong_name * thm) list * cong_name list,
-    procs: proc Net.net,
-    mk_rews:
-     {mk: Proof.context -> thm -> thm list,
-      mk_cong: Proof.context -> thm -> thm,
-      mk_sym: Proof.context -> thm -> thm option,
-      mk_eq_True: Proof.context -> thm -> thm option,
-      reorient: Proof.context -> term list -> term -> term -> bool},
-    term_ord: term ord,
-    subgoal_tac: Proof.context -> int -> tactic,
-    loop_tacs: (string * (Proof.context -> int -> tactic)) list,
-    solvers: solver list * solver list}
+  val subgoal_tac: Proof.context -> int -> tactic
+  val loop_tac: Proof.context -> int -> tactic
+  val solvers: Proof.context -> solver list * solver list
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
@@ -384,6 +374,16 @@
     init_ss depth mk_rews term_ord subgoal_tac solvers);
 
 
+(* accessors for tactis *)
+
+fun subgoal_tac ctxt = (#subgoal_tac o internal_ss o simpset_of) ctxt ctxt;
+
+fun loop_tac ctxt =
+  FIRST' (map (fn (_, tac) => tac ctxt) (rev ((#loop_tacs o internal_ss o simpset_of) ctxt)));
+
+val solvers = #solvers o internal_ss o simpset_of
+
+
 (* simp depth *)
 
 (*
diff -r f1838cf9f139 -r d12c58e12c51 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Dec 04 20:25:21 2019 +0000
+++ b/src/Pure/simplifier.ML	Thu Dec 05 09:24:34 2019 +0000
@@ -197,16 +197,15 @@
 
 fun solve_all_tac solvers ctxt =
   let
-    val {subgoal_tac, ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
-    val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt) THEN_ALL_NEW (K no_tac);
+    val subgoal_tac = Raw_Simplifier.subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt);
+    val solve_tac = subgoal_tac THEN_ALL_NEW (K no_tac);
   in DEPTH_SOLVE (solve_tac 1) end;
 
 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
 fun generic_simp_tac safe mode ctxt =
   let
-    val {loop_tacs, solvers = (unsafe_solvers, solvers), ...} =
-      Raw_Simplifier.internal_ss (simpset_of ctxt);
-    val loop_tac = FIRST' (map (fn (_, tac) => tac ctxt) (rev loop_tacs));
+    val loop_tac = Raw_Simplifier.loop_tac ctxt;
+    val (unsafe_solvers, solvers) = Raw_Simplifier.solvers ctxt;
     val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
       (rev (if safe then solvers else unsafe_solvers)));
 
@@ -219,7 +218,7 @@
 
 fun simp rew mode ctxt thm =
   let
-    val {solvers = (unsafe_solvers, _), ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
+    val (unsafe_solvers, _) = Raw_Simplifier.solvers ctxt;
     val tacf = solve_all_tac (rev unsafe_solvers);
     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   in rew mode prover ctxt thm end;