1.1 --- a/src/FOL/simpdata.ML	Wed Jun 29 18:12:34 2011 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
     1.3 @@ -108,10 +108,10 @@
     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 prems = FIRST'[resolve_tac (triv_rls @ prems),
     1.8 +fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
     1.9                                   atac, etac @{thm FalseE}];
    1.10  (*No premature instantiation of variables during simplification*)
    1.11 -fun   safe_solver prems = FIRST'[match_tac (triv_rls @ prems),
    1.12 +fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
    1.13                                   eq_assume_tac, ematch_tac [@{thm FalseE}]];
    1.14  
    1.15  (*No simprules, but basic infastructure for simplification*)

     2.1 --- a/src/HOL/Orderings.thy	Wed Jun 29 18:12:34 2011 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Wed Jun 29 20:39:41 2011 +0200
     2.3 @@ -570,7 +570,7 @@
     2.4  
     2.5  fun add_solver name tac =
     2.6    Simplifier.map_simpset_global (fn ss => ss addSolver
     2.7 -    mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
     2.8 +    mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
     2.9  
    2.10  in
    2.11    add_simprocs [

     3.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Jun 29 18:12:34 2011 +0200
     3.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Jun 29 20:39:41 2011 +0200
     3.3 @@ -352,10 +352,8 @@
     3.4          | NONE => no_tac)
     3.5      | _ => no_tac))
     3.6  
     3.7 -fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
     3.8 -     (fn ss => case try Simplifier.the_context ss of
     3.9 -                 SOME ctxt => distinctTree_tac names ctxt
    3.10 -               | NONE => K no_tac)
    3.11 +fun distinctFieldSolver names = mk_solver "distinctFieldSolver"
    3.12 +     (distinctTree_tac names o Simplifier.the_context)
    3.13  
    3.14  fun distinct_simproc names =
    3.15    Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]

     4.1 --- a/src/HOL/Statespace/state_space.ML	Wed Jun 29 18:12:34 2011 +0200
     4.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Jun 29 20:39:41 2011 +0200
     4.3 @@ -225,10 +225,8 @@
     4.4        | NONE => no_tac)
     4.5    | _ => no_tac));
     4.6  
     4.7 -val distinctNameSolver = mk_solver' "distinctNameSolver"
     4.8 -     (fn ss => case try Simplifier.the_context ss of
     4.9 -                 SOME ctxt => distinctTree_tac ctxt
    4.10 -                | NONE => K no_tac)
    4.11 +val distinctNameSolver = mk_solver "distinctNameSolver"
    4.12 +     (distinctTree_tac o Simplifier.the_context)
    4.13  
    4.14  val distinct_simproc =
    4.15    Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]

     5.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Jun 29 18:12:34 2011 +0200
     5.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Jun 29 20:39:41 2011 +0200
     5.3 @@ -225,7 +225,7 @@
     5.4  *)
     5.5  ML {*
     5.6    val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
     5.7 -  val fast_solver = mk_solver' "fast_solver" (fn ss =>
     5.8 +  val fast_solver = mk_solver "fast_solver" (fn ss =>
     5.9      if Config.get (Simplifier.the_context ss) config_fast_solver
    5.10      then assume_tac ORELSE' (etac notE)
    5.11      else K no_tac);

     6.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jun 29 18:12:34 2011 +0200
     6.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jun 29 20:39:41 2011 +0200
     6.3 @@ -55,7 +55,7 @@
     6.4    REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
     6.5  
     6.6  fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
     6.7 -val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
     6.8 +val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
     6.9  
    6.10  fun quotient_tac ctxt =
    6.11    (REPEAT_ALL_NEW (FIRST'
    6.12 @@ -63,8 +63,7 @@
    6.13       resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
    6.14  
    6.15  fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
    6.16 -val quotient_solver =
    6.17 -  Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
    6.18 +val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
    6.19  
    6.20  fun solve_quotient_assm ctxt thm =
    6.21    case Seq.pull (quotient_tac ctxt 1 thm) of

     7.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Jun 29 18:12:34 2011 +0200
     7.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 29 20:39:41 2011 +0200
     7.3 @@ -895,7 +895,7 @@
     7.4  val setup =
     7.5    init_arith_data #>
     7.6    Simplifier.map_ss (fn ss => ss
     7.7 -    addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
     7.8 +    addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
     7.9  
    7.10  val global_setup =
    7.11    Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))

     8.1 --- a/src/HOL/Tools/simpdata.ML	Wed Jun 29 18:12:34 2011 +0200
     8.2 +++ b/src/HOL/Tools/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
     8.3 @@ -112,18 +112,18 @@
     8.4  fun mksimps pairs (_: simpset) =
     8.5    map_filter (try mk_eq) o mk_atomize pairs o gen_all;
     8.6  
     8.7 -fun unsafe_solver_tac prems =
     8.8 +fun unsafe_solver_tac ss =
     8.9    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
    8.10 -  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), atac,
    8.11 +  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss), atac,
    8.12      etac @{thm FalseE}];
    8.13  
    8.14  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    8.15  
    8.16  
    8.17  (*No premature instantiation of variables during simplification*)
    8.18 -fun safe_solver_tac prems =
    8.19 +fun safe_solver_tac ss =
    8.20    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
    8.21 -  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems),
    8.22 +  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss),
    8.23           eq_assume_tac, ematch_tac @{thms FalseE}];
    8.24  
    8.25  val safe_solver = mk_solver "HOL safe" safe_solver_tac;

     9.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jun 29 18:12:34 2011 +0200
     9.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jun 29 20:39:41 2011 +0200
     9.3 @@ -1029,10 +1029,10 @@
     9.4  
     9.5  setup {*
     9.6    Simplifier.map_simpset_global (fn ss => ss
     9.7 -    addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
     9.8 -    addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
     9.9 -    addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
    9.10 -    addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
    9.11 +    addSolver (mk_solver "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
    9.12 +    addSolver (mk_solver "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
    9.13 +    addSolver (mk_solver "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
    9.14 +    addSolver (mk_solver "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
    9.15  *}
    9.16  
    9.17  

    10.1 --- a/src/Pure/raw_simplifier.ML	Wed Jun 29 18:12:34 2011 +0200
    10.2 +++ b/src/Pure/raw_simplifier.ML	Wed Jun 29 20:39:41 2011 +0200
    10.3 @@ -20,8 +20,7 @@
    10.4    type simpset
    10.5    type proc
    10.6    type solver
    10.7 -  val mk_solver': string -> (simpset -> int -> tactic) -> solver
    10.8 -  val mk_solver: string -> (thm list -> int -> tactic) -> solver
    10.9 +  val mk_solver: string -> (simpset -> int -> tactic) -> solver
   10.10    val empty_ss: simpset
   10.11    val merge_ss: simpset * simpset -> simpset
   10.12    val dest_ss: simpset ->
   10.13 @@ -242,8 +241,7 @@
   10.14    s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
   10.15  fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
   10.16  
   10.17 -fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
   10.18 -fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
   10.19 +fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()};
   10.20  
   10.21  fun solver_name (Solver {name, ...}) = name;
   10.22  fun solver ss (Solver {solver = tac, ...}) = tac ss;

    11.1 --- a/src/Pure/simplifier.ML	Wed Jun 29 18:12:34 2011 +0200
    11.2 +++ b/src/Pure/simplifier.ML	Wed Jun 29 20:39:41 2011 +0200
    11.3 @@ -396,11 +396,11 @@
    11.4    let
    11.5      val trivialities = Drule.reflexive_thm :: trivs;
    11.6  
    11.7 -    fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
    11.8 +    fun unsafe_solver_tac ss = FIRST' [resolve_tac (trivialities @ prems_of_ss ss), assume_tac];
    11.9      val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   11.10  
   11.11      (*no premature instantiation of variables during simplification*)
   11.12 -    fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
   11.13 +    fun safe_solver_tac ss = FIRST' [match_tac (trivialities @ prems_of_ss ss), eq_assume_tac];
   11.14      val safe_solver = mk_solver "easy safe" safe_solver_tac;
   11.15  
   11.16      fun mk_eq thm =

    12.1 --- a/src/Sequents/simpdata.ML	Wed Jun 29 18:12:34 2011 +0200
    12.2 +++ b/src/Sequents/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
    12.3 @@ -58,12 +58,12 @@
    12.4  val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
    12.5    @{thm iff_refl}, reflexive_thm];
    12.6  
    12.7 -fun unsafe_solver prems =
    12.8 -  FIRST' [resolve_tac (triv_rls @ prems), assume_tac];
    12.9 +fun unsafe_solver ss =
   12.10 +  FIRST' [resolve_tac (triv_rls @ prems_of_ss ss), assume_tac];
   12.11  
   12.12  (*No premature instantiation of variables during simplification*)
   12.13 -fun safe_solver prems =
   12.14 - FIRST' [fn i => DETERM (match_tac (triv_rls @ prems) i), eq_assume_tac];
   12.15 +fun safe_solver ss =
   12.16 + FIRST' [fn i => DETERM (match_tac (triv_rls @ prems_of_ss ss) i), eq_assume_tac];
   12.17  
   12.18  (*No simprules, but basic infrastructure for simplification*)
   12.19  val LK_basic_ss =

    13.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Jun 29 18:12:34 2011 +0200
    13.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Jun 29 20:39:41 2011 +0200
    13.3 @@ -329,7 +329,7 @@
    13.4       val min_ss = Simplifier.global_context thy empty_ss
    13.5             setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    13.6             setSolver (mk_solver "minimal"
    13.7 -                      (fn prems => resolve_tac (triv_rls@prems)
    13.8 +                      (fn ss => resolve_tac (triv_rls @ prems_of_ss ss)
    13.9                                     ORELSE' assume_tac
   13.10                                     ORELSE' etac @{thm FalseE}));
   13.11  

    14.1 --- a/src/ZF/Tools/typechk.ML	Wed Jun 29 18:12:34 2011 +0200
    14.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jun 29 20:39:41 2011 +0200
    14.3 @@ -105,8 +105,9 @@
    14.4                    ORELSE (ares_tac hyps 1
    14.5                            APPEND typecheck_step_tac (tcset_of ctxt))));
    14.6  
    14.7 -val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss =>
    14.8 -  type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss));
    14.9 +val type_solver =
   14.10 +  Simplifier.mk_solver "ZF typecheck" (fn ss =>
   14.11 +    type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss));
   14.12  
   14.13  
   14.14  (* concrete syntax *)