--- a/src/FOL/simpdata.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/FOL/simpdata.ML Wed Jun 29 20:39:41 2011 +0200
@@ -108,10 +108,10 @@
val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
-fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls @ prems),
+fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
atac, etac @{thm FalseE}];
(*No premature instantiation of variables during simplification*)
-fun safe_solver prems = FIRST'[match_tac (triv_rls @ prems),
+fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
eq_assume_tac, ematch_tac [@{thm FalseE}]];
(*No simprules, but basic infastructure for simplification*)
--- a/src/HOL/Orderings.thy Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/Orderings.thy Wed Jun 29 20:39:41 2011 +0200
@@ -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) (Simplifier.prems_of_ss ss)));
+ mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
in
add_simprocs [
--- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Jun 29 20:39:41 2011 +0200
@@ -352,10 +352,8 @@
| NONE => no_tac)
| _ => no_tac))
-fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
- (fn ss => case try Simplifier.the_context ss of
- SOME ctxt => distinctTree_tac names ctxt
- | NONE => K no_tac)
+fun distinctFieldSolver names = mk_solver "distinctFieldSolver"
+ (distinctTree_tac names o Simplifier.the_context)
fun distinct_simproc names =
Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
--- a/src/HOL/Statespace/state_space.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Jun 29 20:39:41 2011 +0200
@@ -225,10 +225,8 @@
| NONE => no_tac)
| _ => no_tac));
-val distinctNameSolver = mk_solver' "distinctNameSolver"
- (fn ss => case try Simplifier.the_context ss of
- SOME ctxt => distinctTree_tac ctxt
- | NONE => K no_tac)
+val distinctNameSolver = mk_solver "distinctNameSolver"
+ (distinctTree_tac o Simplifier.the_context)
val distinct_simproc =
Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Jun 29 20:39:41 2011 +0200
@@ -225,7 +225,7 @@
*)
ML {*
val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
- val fast_solver = mk_solver' "fast_solver" (fn ss =>
+ val fast_solver = mk_solver "fast_solver" (fn ss =>
if Config.get (Simplifier.the_context ss) config_fast_solver
then assume_tac ORELSE' (etac notE)
else K no_tac);
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jun 29 20:39:41 2011 +0200
@@ -55,7 +55,7 @@
REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
-val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
@@ -63,8 +63,7 @@
resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver =
- Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
fun solve_quotient_assm ctxt thm =
case Seq.pull (quotient_tac ctxt 1 thm) of
--- a/src/HOL/Tools/lin_arith.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Jun 29 20:39:41 2011 +0200
@@ -895,7 +895,7 @@
val setup =
init_arith_data #>
Simplifier.map_ss (fn ss => ss
- addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
+ addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
val global_setup =
Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
--- a/src/HOL/Tools/simpdata.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML Wed Jun 29 20:39:41 2011 +0200
@@ -112,18 +112,18 @@
fun mksimps pairs (_: simpset) =
map_filter (try mk_eq) o mk_atomize pairs o gen_all;
-fun unsafe_solver_tac prems =
+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), atac,
+ FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss), atac,
etac @{thm FalseE}];
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
(*No premature instantiation of variables during simplification*)
-fun safe_solver_tac prems =
+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),
+ FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss),
eq_assume_tac, ematch_tac @{thms FalseE}];
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
--- a/src/HOL/Transitive_Closure.thy Wed Jun 29 18:12:34 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy Wed Jun 29 20:39:41 2011 +0200
@@ -1029,10 +1029,10 @@
setup {*
Simplifier.map_simpset_global (fn ss => ss
- addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
- addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
- addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
- addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
+ addSolver (mk_solver "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
+ addSolver (mk_solver "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
+ addSolver (mk_solver "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
+ addSolver (mk_solver "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
*}
--- a/src/Pure/raw_simplifier.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Wed Jun 29 20:39:41 2011 +0200
@@ -20,8 +20,7 @@
type simpset
type proc
type solver
- val mk_solver': string -> (simpset -> int -> tactic) -> solver
- val mk_solver: string -> (thm list -> int -> tactic) -> solver
+ val mk_solver: string -> (simpset -> int -> tactic) -> solver
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
val dest_ss: simpset ->
@@ -242,8 +241,7 @@
s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
-fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
-fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
+fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()};
fun solver_name (Solver {name, ...}) = name;
fun solver ss (Solver {solver = tac, ...}) = tac ss;
--- a/src/Pure/simplifier.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/Pure/simplifier.ML Wed Jun 29 20:39:41 2011 +0200
@@ -396,11 +396,11 @@
let
val trivialities = Drule.reflexive_thm :: trivs;
- fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
+ fun unsafe_solver_tac ss = FIRST' [resolve_tac (trivialities @ prems_of_ss ss), assume_tac];
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
(*no premature instantiation of variables during simplification*)
- fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
+ fun safe_solver_tac ss = FIRST' [match_tac (trivialities @ prems_of_ss ss), eq_assume_tac];
val safe_solver = mk_solver "easy safe" safe_solver_tac;
fun mk_eq thm =
--- a/src/Sequents/simpdata.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/Sequents/simpdata.ML Wed Jun 29 20:39:41 2011 +0200
@@ -58,12 +58,12 @@
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
@{thm iff_refl}, reflexive_thm];
-fun unsafe_solver prems =
- FIRST' [resolve_tac (triv_rls @ prems), assume_tac];
+fun unsafe_solver ss =
+ FIRST' [resolve_tac (triv_rls @ prems_of_ss ss), assume_tac];
(*No premature instantiation of variables during simplification*)
-fun safe_solver prems =
- FIRST' [fn i => DETERM (match_tac (triv_rls @ prems) i), eq_assume_tac];
+fun safe_solver ss =
+ FIRST' [fn i => DETERM (match_tac (triv_rls @ prems_of_ss ss) i), eq_assume_tac];
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =
--- a/src/ZF/Tools/inductive_package.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Jun 29 20:39:41 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 prems => resolve_tac (triv_rls@prems)
+ (fn ss => resolve_tac (triv_rls @ prems_of_ss ss)
ORELSE' assume_tac
ORELSE' etac @{thm FalseE}));
--- a/src/ZF/Tools/typechk.ML Wed Jun 29 18:12:34 2011 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Jun 29 20:39:41 2011 +0200
@@ -105,8 +105,9 @@
ORELSE (ares_tac hyps 1
APPEND typecheck_step_tac (tcset_of ctxt))));
-val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss =>
- type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss));
+val type_solver =
+ Simplifier.mk_solver "ZF typecheck" (fn ss =>
+ type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss));
(* concrete syntax *)