# HG changeset patch
# User wenzelm
# Date 1309376056 -7200
# Node ID b4a093e755db050666fe348217ed4f7b549887ce
# Parent  78211f66cf8d6b9e3274e3cbbcd24ca61e024917
tuned signature;

diff -r 78211f66cf8d -r b4a093e755db src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/FOL/simpdata.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -108,11 +108,12 @@
 
 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
 
-fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
-                                 atac, etac @{thm FalseE}];
+fun unsafe_solver ss =
+  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), atac, etac @{thm FalseE}];
+
 (*No premature instantiation of variables during simplification*)
-fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
-                                 eq_assume_tac, ematch_tac [@{thm FalseE}]];
+fun safe_solver ss =
+  FIRST' [match_tac (triv_rls @ Simplifier.prems_of ss), eq_assume_tac, ematch_tac @{thms FalseE}];
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
diff -r 78211f66cf8d -r b4a093e755db src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/HOL.thy	Wed Jun 29 21:34:16 2011 +0200
@@ -1232,7 +1232,7 @@
   fun proc ss ct =
     (case Thm.term_of ct of
       eq $ lhs $ rhs =>
-        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of_ss ss) of
+        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
           SOME thm => SOME (thm RS neq_to_EQ_False)
         | NONE => NONE)
      | _ => NONE);
diff -r 78211f66cf8d -r b4a093e755db src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Orderings.thy	Wed Jun 29 21:34:16 2011 +0200
@@ -534,7 +534,7 @@
 fun prp t thm = (#prop (rep_thm thm) = t);
 
 fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
-  let val prems = prems_of_ss ss;
+  let val prems = Simplifier.prems_of ss;
       val less = Const (@{const_name less}, T);
       val t = HOLogic.mk_Trueprop(le $ s $ r);
   in case find_first (prp t) prems of
@@ -549,7 +549,7 @@
   handle THM _ => NONE;
 
 fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
-  let val prems = prems_of_ss ss;
+  let val prems = Simplifier.prems_of ss;
       val le = Const (@{const_name less_eq}, T);
       val t = HOLogic.mk_Trueprop(le $ r $ s);
   in case find_first (prp t) prems of
@@ -570,7 +570,7 @@
 
 fun add_solver name tac =
   Simplifier.map_simpset_global (fn ss => ss addSolver
-    mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
+    mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss)));
 
 in
   add_simprocs [
diff -r 78211f66cf8d -r b4a093e755db src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -307,7 +307,7 @@
     let
       val (le, r, s) = dest_binop t
       val less = Const (@{const_name less}, Term.fastype_of le)
-      val prems = Simplifier.prems_of_ss ss
+      val prems = Simplifier.prems_of ss
     in
       (case find_first (eq_prop (le $ s $ r)) prems of
         NONE =>
@@ -321,7 +321,7 @@
     let
       val (less, r, s) = dest_binop (HOLogic.dest_not t)
       val le = Const (@{const_name less_eq}, Term.fastype_of less)
-      val prems = prems_of_ss ss
+      val prems = Simplifier.prems_of ss
     in
       (case find_first (eq_prop (le $ r $ s)) prems of
         NONE =>
diff -r 78211f66cf8d -r b4a093e755db src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -657,7 +657,7 @@
      fun prover used ss thm =
      let fun cong_prover ss thm =
          let val dummy = say "cong_prover:"
-             val cntxt = Simplifier.prems_of_ss ss
+             val cntxt = Simplifier.prems_of ss
              val dummy = print_thms "cntxt:" cntxt
              val dummy = say "cong rule:"
              val dummy = say (Display.string_of_thm_without_context thm)
@@ -739,7 +739,7 @@
 
         fun restrict_prover ss thm =
           let val dummy = say "restrict_prover:"
-              val cntxt = rev(Simplifier.prems_of_ss ss)
+              val cntxt = rev (Simplifier.prems_of ss)
               val dummy = print_thms "cntxt:" cntxt
               val thy = Thm.theory_of_thm thm
               val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
diff -r 78211f66cf8d -r b4a093e755db src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -114,8 +114,8 @@
 
 fun unsafe_solver_tac ss =
   (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
-  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss), atac,
-    etac @{thm FalseE}];
+  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
+    atac, etac @{thm FalseE}];
 
 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
 
@@ -123,8 +123,8 @@
 (*No premature instantiation of variables during simplification*)
 fun safe_solver_tac ss =
   (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
-  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss),
-         eq_assume_tac, ematch_tac @{thms FalseE}];
+  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
+    eq_assume_tac, ematch_tac @{thms FalseE}];
 
 val safe_solver = mk_solver "HOL safe" safe_solver_tac;
 
diff -r 78211f66cf8d -r b4a093e755db src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -47,7 +47,7 @@
 fun proc ss t =
   let
     val ctxt = Simplifier.the_context ss;
-    val prems = prems_of_ss ss;
+    val prems = Simplifier.prems_of ss;
     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
     val export = singleton (Variable.export ctxt' ctxt)
 
diff -r 78211f66cf8d -r b4a093e755db src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -68,7 +68,7 @@
 fun proc ss t =
   let
     val ctxt = Simplifier.the_context ss
-    val prems = prems_of_ss ss
+    val prems = Simplifier.prems_of ss
     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
     val export = singleton (Variable.export ctxt' ctxt)
 
diff -r 78211f66cf8d -r b4a093e755db src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/extract_common_term.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -49,7 +49,7 @@
 fun proc ss t =
   let
     val ctxt = Simplifier.the_context ss;
-    val prems = prems_of_ss ss;
+    val prems = Simplifier.prems_of ss;
     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
     val export = singleton (Variable.export ctxt' ctxt)
 
diff -r 78211f66cf8d -r b4a093e755db src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -835,7 +835,7 @@
   end);
 
 fun cut_lin_arith_tac ss =
-  cut_facts_tac (Simplifier.prems_of_ss ss) THEN'
+  cut_facts_tac (Simplifier.prems_of ss) THEN'
   simpset_lin_arith_tac ss false;
 
 fun lin_arith_tac ctxt =
@@ -916,7 +916,7 @@
 fun lin_arith_simproc ss concl =
   let
     val ctxt = Simplifier.the_context ss
-    val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss)
+    val thms = maps LA_Logic.atomize (Simplifier.prems_of ss)
     val Hs = map Thm.prop_of thms
     val Tconcl = LA_Logic.mk_Trueprop concl
   in
diff -r 78211f66cf8d -r b4a093e755db src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -37,7 +37,6 @@
   val make_simproc: {name: string, lhss: cterm list,
     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
   val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
-  val prems_of_ss: simpset -> thm list
   val addsimps: simpset * thm list -> simpset
   val delsimps: simpset * thm list -> simpset
   val addeqcongs: simpset * thm list -> simpset
@@ -97,6 +96,7 @@
     subgoal_tac: simpset -> int -> tactic,
     loop_tacs: (string * (simpset -> int -> tactic)) list,
     solvers: solver list * solver list}
+  val prems_of: simpset -> thm list
   val add_simp: thm -> simpset -> simpset
   val del_simp: thm -> simpset -> simpset
   val solver: simpset -> solver -> int -> tactic
@@ -235,7 +235,7 @@
 fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
 fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
 
-fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
+fun prems_of (Simpset ({prems, ...}, _)) = prems;
 
 fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
   s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
@@ -562,7 +562,7 @@
 
 fun is_full_cong thm =
   let
-    val prems = prems_of thm and concl = concl_of thm;
+    val prems = Thm.prems_of thm and concl = Thm.concl_of thm;
     val (lhs, rhs) = Logic.dest_equals concl;
     val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
   in
@@ -1278,7 +1278,7 @@
   in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
 
 val simple_prover =
-  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
+  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of ss)));
 
 fun rewrite _ [] ct = Thm.reflexive ct
   | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
diff -r 78211f66cf8d -r b4a093e755db src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Pure/simplifier.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -34,6 +34,7 @@
   val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
   val debug_bounds: bool Unsynchronized.ref
+  val prems_of: simpset -> thm list
   val add_simp: thm -> simpset -> simpset
   val del_simp: thm -> simpset -> simpset
   val add_prems: thm list -> simpset -> simpset
@@ -396,11 +397,13 @@
   let
     val trivialities = Drule.reflexive_thm :: trivs;
 
-    fun unsafe_solver_tac ss = FIRST' [resolve_tac (trivialities @ prems_of_ss ss), assume_tac];
+    fun unsafe_solver_tac ss =
+      FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ss), assume_tac];
     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
 
     (*no premature instantiation of variables during simplification*)
-    fun safe_solver_tac ss = FIRST' [match_tac (trivialities @ prems_of_ss ss), eq_assume_tac];
+    fun safe_solver_tac ss =
+      FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ss), eq_assume_tac];
     val safe_solver = mk_solver "easy safe" safe_solver_tac;
 
     fun mk_eq thm =
diff -r 78211f66cf8d -r b4a093e755db src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Sequents/simpdata.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -59,11 +59,11 @@
   @{thm iff_refl}, reflexive_thm];
 
 fun unsafe_solver ss =
-  FIRST' [resolve_tac (triv_rls @ prems_of_ss ss), assume_tac];
+  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), assume_tac];
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ss =
- FIRST' [fn i => DETERM (match_tac (triv_rls @ prems_of_ss ss) i), eq_assume_tac];
+ FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ss) i), eq_assume_tac];
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
diff -r 78211f66cf8d -r b4a093e755db src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -329,7 +329,7 @@
      val min_ss = Simplifier.global_context thy empty_ss
            setmksimps (K (map mk_eq o ZF_atomize o gen_all))
            setSolver (mk_solver "minimal"
-                      (fn ss => resolve_tac (triv_rls @ prems_of_ss ss)
+                      (fn ss => resolve_tac (triv_rls @ Simplifier.prems_of ss)
                                    ORELSE' assume_tac
                                    ORELSE' etac @{thm FalseE}));
 
diff -r 78211f66cf8d -r b4a093e755db src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Jun 29 20:39:41 2011 +0200
+++ b/src/ZF/Tools/typechk.ML	Wed Jun 29 21:34:16 2011 +0200
@@ -107,7 +107,7 @@
 
 val type_solver =
   Simplifier.mk_solver "ZF typecheck" (fn ss =>
-    type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss));
+    type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of ss));
 
 
 (* concrete syntax *)