# HG changeset patch
# User wenzelm
# Date 1386866090 -3600
# Node ID 445e7947c6b5d3190a381fc320ff33efd273d67d
# Parent  a806e7251cf0d1763b12de280d74495feca4e9fa
tuned signature;

diff -r a806e7251cf0 -r 445e7947c6b5 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Dec 12 16:56:53 2013 +0100
+++ b/src/Pure/raw_simplifier.ML	Thu Dec 12 17:34:50 2013 +0100
@@ -73,10 +73,6 @@
   include BASIC_RAW_SIMPLIFIER
   exception SIMPLIFIER of string * thm
   val internal_ss: simpset ->
-   {rules: rrule Net.net,
-    prems: thm list,
-    bounds: int * ((string * typ) * string) list,
-    depth: int * bool Unsynchronized.ref} *
    {congs: (cong_name * thm) list * cong_name list,
     procs: proc Net.net,
     mk_rews:
@@ -287,7 +283,7 @@
     loop_tacs: (string * (Proof.context -> int -> tactic)) list,
     solvers: solver list * solver list};
 
-fun internal_ss (Simpset args) = args;
+fun internal_ss (Simpset (_, ss2)) = ss2;
 
 fun make_ss1 (rules, prems, bounds, depth) =
   {rules = rules, prems = prems, bounds = bounds, depth = depth};
diff -r a806e7251cf0 -r 445e7947c6b5 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Dec 12 16:56:53 2013 +0100
+++ b/src/Pure/simplifier.ML	Thu Dec 12 17:34:50 2013 +0100
@@ -190,14 +190,14 @@
 
 fun solve_all_tac solvers ctxt =
   let
-    val (_, {subgoal_tac, ...}) = Raw_Simplifier.internal_ss (simpset_of ctxt);
+    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);
   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), ...}) =
+    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 solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
@@ -212,7 +212,7 @@
 
 fun simp rew mode ctxt thm =
   let
-    val (_, {solvers = (unsafe_solvers, _), ...}) = Raw_Simplifier.internal_ss (simpset_of ctxt);
+    val {solvers = (unsafe_solvers, _), ...} = Raw_Simplifier.internal_ss (simpset_of 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;