1.1 --- a/src/FOL/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Jun 29 21:34:16 2011 +0200
     1.3 @@ -108,11 +108,12 @@
     1.4  
     1.5  val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
     1.6  
     1.7 -fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
     1.8 -                                 atac, etac @{thm FalseE}];
     1.9 +fun unsafe_solver ss =
    1.10 +  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), atac, etac @{thm FalseE}];
    1.11 +
    1.12  (*No premature instantiation of variables during simplification*)
    1.13 -fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
    1.14 -                                 eq_assume_tac, ematch_tac [@{thm FalseE}]];
    1.15 +fun safe_solver ss =
    1.16 +  FIRST' [match_tac (triv_rls @ Simplifier.prems_of ss), eq_assume_tac, ematch_tac @{thms FalseE}];
    1.17  
    1.18  (*No simprules, but basic infastructure for simplification*)
    1.19  val FOL_basic_ss =

     2.1 --- a/src/HOL/HOL.thy	Wed Jun 29 20:39:41 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Jun 29 21:34:16 2011 +0200
     2.3 @@ -1232,7 +1232,7 @@
     2.4    fun proc ss ct =
     2.5      (case Thm.term_of ct of
     2.6        eq $ lhs $ rhs =>
     2.7 -        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of_ss ss) of
     2.8 +        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
     2.9            SOME thm => SOME (thm RS neq_to_EQ_False)
    2.10          | NONE => NONE)
    2.11       | _ => NONE);

     3.1 --- a/src/HOL/Orderings.thy	Wed Jun 29 20:39:41 2011 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Wed Jun 29 21:34:16 2011 +0200
     3.3 @@ -534,7 +534,7 @@
     3.4  fun prp t thm = (#prop (rep_thm thm) = t);
     3.5  
     3.6  fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
     3.7 -  let val prems = prems_of_ss ss;
     3.8 +  let val prems = Simplifier.prems_of ss;
     3.9        val less = Const (@{const_name less}, T);
    3.10        val t = HOLogic.mk_Trueprop(le $ s $ r);
    3.11    in case find_first (prp t) prems of
    3.12 @@ -549,7 +549,7 @@
    3.13    handle THM _ => NONE;
    3.14  
    3.15  fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
    3.16 -  let val prems = prems_of_ss ss;
    3.17 +  let val prems = Simplifier.prems_of ss;
    3.18        val le = Const (@{const_name less_eq}, T);
    3.19        val t = HOLogic.mk_Trueprop(le $ r $ s);
    3.20    in case find_first (prp t) prems of
    3.21 @@ -570,7 +570,7 @@
    3.22  
    3.23  fun add_solver name tac =
    3.24    Simplifier.map_simpset_global (fn ss => ss addSolver
    3.25 -    mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
    3.26 +    mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss)));
    3.27  
    3.28  in
    3.29    add_simprocs [

     4.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Jun 29 20:39:41 2011 +0200
     4.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Jun 29 21:34:16 2011 +0200
     4.3 @@ -307,7 +307,7 @@
     4.4      let
     4.5        val (le, r, s) = dest_binop t
     4.6        val less = Const (@{const_name less}, Term.fastype_of le)
     4.7 -      val prems = Simplifier.prems_of_ss ss
     4.8 +      val prems = Simplifier.prems_of ss
     4.9      in
    4.10        (case find_first (eq_prop (le $ s $ r)) prems of
    4.11          NONE =>
    4.12 @@ -321,7 +321,7 @@
    4.13      let
    4.14        val (less, r, s) = dest_binop (HOLogic.dest_not t)
    4.15        val le = Const (@{const_name less_eq}, Term.fastype_of less)
    4.16 -      val prems = prems_of_ss ss
    4.17 +      val prems = Simplifier.prems_of ss
    4.18      in
    4.19        (case find_first (eq_prop (le $ r $ s)) prems of
    4.20          NONE =>

     5.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Jun 29 20:39:41 2011 +0200
     5.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Jun 29 21:34:16 2011 +0200
     5.3 @@ -657,7 +657,7 @@
     5.4       fun prover used ss thm =
     5.5       let fun cong_prover ss thm =
     5.6           let val dummy = say "cong_prover:"
     5.7 -             val cntxt = Simplifier.prems_of_ss ss
     5.8 +             val cntxt = Simplifier.prems_of ss
     5.9               val dummy = print_thms "cntxt:" cntxt
    5.10               val dummy = say "cong rule:"
    5.11               val dummy = say (Display.string_of_thm_without_context thm)
    5.12 @@ -739,7 +739,7 @@
    5.13  
    5.14          fun restrict_prover ss thm =
    5.15            let val dummy = say "restrict_prover:"
    5.16 -              val cntxt = rev(Simplifier.prems_of_ss ss)
    5.17 +              val cntxt = rev (Simplifier.prems_of ss)
    5.18                val dummy = print_thms "cntxt:" cntxt
    5.19                val thy = Thm.theory_of_thm thm
    5.20                val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm

     6.1 --- a/src/HOL/Tools/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
     6.2 +++ b/src/HOL/Tools/simpdata.ML	Wed Jun 29 21:34:16 2011 +0200
     6.3 @@ -114,8 +114,8 @@
     6.4  
     6.5  fun unsafe_solver_tac ss =
     6.6    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
     6.7 -  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss), atac,
     6.8 -    etac @{thm FalseE}];
     6.9 +  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
    6.10 +    atac, etac @{thm FalseE}];
    6.11  
    6.12  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    6.13  
    6.14 @@ -123,8 +123,8 @@
    6.15  (*No premature instantiation of variables during simplification*)
    6.16  fun safe_solver_tac ss =
    6.17    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
    6.18 -  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss),
    6.19 -         eq_assume_tac, ematch_tac @{thms FalseE}];
    6.20 +  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
    6.21 +    eq_assume_tac, ematch_tac @{thms FalseE}];
    6.22  
    6.23  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
    6.24  

     7.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Wed Jun 29 20:39:41 2011 +0200
     7.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Wed Jun 29 21:34:16 2011 +0200
     7.3 @@ -47,7 +47,7 @@
     7.4  fun proc ss t =
     7.5    let
     7.6      val ctxt = Simplifier.the_context ss;
     7.7 -    val prems = prems_of_ss ss;
     7.8 +    val prems = Simplifier.prems_of ss;
     7.9      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    7.10      val export = singleton (Variable.export ctxt' ctxt)
    7.11  

     8.1 --- a/src/Provers/Arith/cancel_numerals.ML	Wed Jun 29 20:39:41 2011 +0200
     8.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Wed Jun 29 21:34:16 2011 +0200
     8.3 @@ -68,7 +68,7 @@
     8.4  fun proc ss t =
     8.5    let
     8.6      val ctxt = Simplifier.the_context ss
     8.7 -    val prems = prems_of_ss ss
     8.8 +    val prems = Simplifier.prems_of ss
     8.9      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    8.10      val export = singleton (Variable.export ctxt' ctxt)
    8.11  

     9.1 --- a/src/Provers/Arith/extract_common_term.ML	Wed Jun 29 20:39:41 2011 +0200
     9.2 +++ b/src/Provers/Arith/extract_common_term.ML	Wed Jun 29 21:34:16 2011 +0200
     9.3 @@ -49,7 +49,7 @@
     9.4  fun proc ss t =
     9.5    let
     9.6      val ctxt = Simplifier.the_context ss;
     9.7 -    val prems = prems_of_ss ss;
     9.8 +    val prems = Simplifier.prems_of ss;
     9.9      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    9.10      val export = singleton (Variable.export ctxt' ctxt)
    9.11  

    10.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 29 20:39:41 2011 +0200
    10.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 29 21:34:16 2011 +0200
    10.3 @@ -835,7 +835,7 @@
    10.4    end);
    10.5  
    10.6  fun cut_lin_arith_tac ss =
    10.7 -  cut_facts_tac (Simplifier.prems_of_ss ss) THEN'
    10.8 +  cut_facts_tac (Simplifier.prems_of ss) THEN'
    10.9    simpset_lin_arith_tac ss false;
   10.10  
   10.11  fun lin_arith_tac ctxt =
   10.12 @@ -916,7 +916,7 @@
   10.13  fun lin_arith_simproc ss concl =
   10.14    let
   10.15      val ctxt = Simplifier.the_context ss
   10.16 -    val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss)
   10.17 +    val thms = maps LA_Logic.atomize (Simplifier.prems_of ss)
   10.18      val Hs = map Thm.prop_of thms
   10.19      val Tconcl = LA_Logic.mk_Trueprop concl
   10.20    in

    11.1 --- a/src/Pure/raw_simplifier.ML	Wed Jun 29 20:39:41 2011 +0200
    11.2 +++ b/src/Pure/raw_simplifier.ML	Wed Jun 29 21:34:16 2011 +0200
    11.3 @@ -37,7 +37,6 @@
    11.4    val make_simproc: {name: string, lhss: cterm list,
    11.5      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
    11.6    val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
    11.7 -  val prems_of_ss: simpset -> thm list
    11.8    val addsimps: simpset * thm list -> simpset
    11.9    val delsimps: simpset * thm list -> simpset
   11.10    val addeqcongs: simpset * thm list -> simpset
   11.11 @@ -97,6 +96,7 @@
   11.12      subgoal_tac: simpset -> int -> tactic,
   11.13      loop_tacs: (string * (simpset -> int -> tactic)) list,
   11.14      solvers: solver list * solver list}
   11.15 +  val prems_of: simpset -> thm list
   11.16    val add_simp: thm -> simpset -> simpset
   11.17    val del_simp: thm -> simpset -> simpset
   11.18    val solver: simpset -> solver -> int -> tactic
   11.19 @@ -235,7 +235,7 @@
   11.20  fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
   11.21  fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
   11.22  
   11.23 -fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
   11.24 +fun prems_of (Simpset ({prems, ...}, _)) = prems;
   11.25  
   11.26  fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
   11.27    s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
   11.28 @@ -562,7 +562,7 @@
   11.29  
   11.30  fun is_full_cong thm =
   11.31    let
   11.32 -    val prems = prems_of thm and concl = concl_of thm;
   11.33 +    val prems = Thm.prems_of thm and concl = Thm.concl_of thm;
   11.34      val (lhs, rhs) = Logic.dest_equals concl;
   11.35      val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
   11.36    in
   11.37 @@ -1278,7 +1278,7 @@
   11.38    in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
   11.39  
   11.40  val simple_prover =
   11.41 -  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
   11.42 +  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of ss)));
   11.43  
   11.44  fun rewrite _ [] ct = Thm.reflexive ct
   11.45    | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover

    12.1 --- a/src/Pure/simplifier.ML	Wed Jun 29 20:39:41 2011 +0200
    12.2 +++ b/src/Pure/simplifier.ML	Wed Jun 29 21:34:16 2011 +0200
    12.3 @@ -34,6 +34,7 @@
    12.4    val pretty_ss: Proof.context -> simpset -> Pretty.T
    12.5    val clear_ss: simpset -> simpset
    12.6    val debug_bounds: bool Unsynchronized.ref
    12.7 +  val prems_of: simpset -> thm list
    12.8    val add_simp: thm -> simpset -> simpset
    12.9    val del_simp: thm -> simpset -> simpset
   12.10    val add_prems: thm list -> simpset -> simpset
   12.11 @@ -396,11 +397,13 @@
   12.12    let
   12.13      val trivialities = Drule.reflexive_thm :: trivs;
   12.14  
   12.15 -    fun unsafe_solver_tac ss = FIRST' [resolve_tac (trivialities @ prems_of_ss ss), assume_tac];
   12.16 +    fun unsafe_solver_tac ss =
   12.17 +      FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ss), assume_tac];
   12.18      val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   12.19  
   12.20      (*no premature instantiation of variables during simplification*)
   12.21 -    fun safe_solver_tac ss = FIRST' [match_tac (trivialities @ prems_of_ss ss), eq_assume_tac];
   12.22 +    fun safe_solver_tac ss =
   12.23 +      FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ss), eq_assume_tac];
   12.24      val safe_solver = mk_solver "easy safe" safe_solver_tac;
   12.25  
   12.26      fun mk_eq thm =

    13.1 --- a/src/Sequents/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
    13.2 +++ b/src/Sequents/simpdata.ML	Wed Jun 29 21:34:16 2011 +0200
    13.3 @@ -59,11 +59,11 @@
    13.4    @{thm iff_refl}, reflexive_thm];
    13.5  
    13.6  fun unsafe_solver ss =
    13.7 -  FIRST' [resolve_tac (triv_rls @ prems_of_ss ss), assume_tac];
    13.8 +  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), assume_tac];
    13.9  
   13.10  (*No premature instantiation of variables during simplification*)
   13.11  fun safe_solver ss =
   13.12 - FIRST' [fn i => DETERM (match_tac (triv_rls @ prems_of_ss ss) i), eq_assume_tac];
   13.13 + FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ss) i), eq_assume_tac];
   13.14  
   13.15  (*No simprules, but basic infrastructure for simplification*)
   13.16  val LK_basic_ss =

    14.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Jun 29 20:39:41 2011 +0200
    14.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Jun 29 21:34:16 2011 +0200
    14.3 @@ -329,7 +329,7 @@
    14.4       val min_ss = Simplifier.global_context thy empty_ss
    14.5             setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    14.6             setSolver (mk_solver "minimal"
    14.7 -                      (fn ss => resolve_tac (triv_rls @ prems_of_ss ss)
    14.8 +                      (fn ss => resolve_tac (triv_rls @ Simplifier.prems_of ss)
    14.9                                     ORELSE' assume_tac
   14.10                                     ORELSE' etac @{thm FalseE}));
   14.11  

    15.1 --- a/src/ZF/Tools/typechk.ML	Wed Jun 29 20:39:41 2011 +0200
    15.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jun 29 21:34:16 2011 +0200
    15.3 @@ -107,7 +107,7 @@
    15.4  
    15.5  val type_solver =
    15.6    Simplifier.mk_solver "ZF typecheck" (fn ss =>
    15.7 -    type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss));
    15.8 +    type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of ss));
    15.9  
   15.10  
   15.11  (* concrete syntax *)