# HG changeset patch
# User wenzelm
# Date 1236422756 -3600
# Node ID efd1bec4630a0ee257ef59ce039026ba7fb21a6a
# Parent  b3ef64cadcadda3f8d699eee5b6f4a556591d2b5
renamed rep_ss to MetaSimplifier.internal_ss;

diff -r b3ef64cadcad -r efd1bec4630a src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Sat Mar 07 11:32:31 2009 +0100
+++ b/src/Pure/meta_simplifier.ML	Sat Mar 07 11:45:56 2009 +0100
@@ -22,24 +22,6 @@
   type solver
   val mk_solver': string -> (simpset -> int -> tactic) -> solver
   val mk_solver: string -> (thm list -> int -> tactic) -> solver
-  val rep_ss: simpset ->
-   {rules: rrule Net.net,
-    prems: thm list,
-    bounds: int * ((string * typ) * string) list,
-    depth: int * bool ref,
-    context: Proof.context option} *
-   {congs: (string * cong) list * string list,
-    procs: proc Net.net,
-    mk_rews:
-     {mk: thm -> thm list,
-      mk_cong: thm -> thm,
-      mk_sym: thm -> thm option,
-      mk_eq_True: thm -> thm option,
-      reorient: theory -> term list -> term -> term -> bool},
-    termless: term * term -> bool,
-    subgoal_tac: simpset -> int -> tactic,
-    loop_tacs: (string * (simpset -> int -> tactic)) list,
-    solvers: solver list * solver list}
   val empty_ss: simpset
   val merge_ss: simpset * simpset -> simpset
   val pretty_ss: simpset -> Pretty.T
@@ -90,6 +72,24 @@
 sig
   include BASIC_META_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 ref,
+    context: Proof.context option} *
+   {congs: (string * cong) list * string list,
+    procs: proc Net.net,
+    mk_rews:
+     {mk: thm -> thm list,
+      mk_cong: thm -> thm,
+      mk_sym: thm -> thm option,
+      mk_eq_True: thm -> thm option,
+      reorient: theory -> term list -> term -> term -> bool},
+    termless: term * term -> bool,
+    subgoal_tac: simpset -> int -> tactic,
+    loop_tacs: (string * (simpset -> int -> tactic)) list,
+    solvers: solver list * solver list}
   val add_simp: thm -> simpset -> simpset
   val del_simp: thm -> simpset -> simpset
   val solver: simpset -> solver -> int -> tactic
@@ -214,7 +214,7 @@
     id: stamp};
 
 
-fun rep_ss (Simpset args) = args;
+fun internal_ss (Simpset args) = args;
 
 fun make_ss1 (rules, prems, bounds, depth, context) =
   {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
@@ -696,7 +696,7 @@
 
 in
 
-val mksimps = #mk o #mk_rews o #2 o rep_ss;
+fun mksimps (Simpset (_, {mk_rews = {mk, ...}, ...})) = mk;
 
 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
diff -r b3ef64cadcad -r efd1bec4630a src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Mar 07 11:32:31 2009 +0100
+++ b/src/Pure/simplifier.ML	Sat Mar 07 11:45:56 2009 +0100
@@ -217,14 +217,14 @@
 
 fun solve_all_tac solvers ss =
   let
-    val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss;
+    val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss;
     val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) 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 ss =
   let
-    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
+    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss;
     val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
     val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
       (rev (if safe then solvers else unsafe_solvers)));
@@ -238,7 +238,7 @@
 
 fun simp rew mode ss thm =
   let
-    val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
+    val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss;
     val tacf = solve_all_tac (rev unsafe_solvers);
     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   in rew mode prover ss thm end;