--- a/src/CCL/Wfd.thy Thu Jul 30 11:23:57 2009 +0200
+++ b/src/CCL/Wfd.thy Thu Jul 30 12:20:43 2009 +0200
@@ -499,7 +499,7 @@
in
fun eval_tac ths =
- FOCUS_PREMS (fn {context, prems, ...} =>
+ Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
val eval_setup =
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jul 30 12:20:43 2009 +0200
@@ -3337,7 +3337,7 @@
REPEAT (FIRST' [etac @{thm intervalE},
etac @{thm meta_eqE},
rtac @{thm impI}] i)
- THEN FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+ THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
THEN TRY (filter_prems_tac (K false) i)
THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
--- a/src/HOL/Prolog/prolog.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Thu Jul 30 12:20:43 2009 +0200
@@ -67,7 +67,7 @@
imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *)
-(*val hyp_resolve_tac = FOCUS_PREMS (fn {prems, ...} =>
+(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
resolve_tac (maps atomizeD prems) 1);
-- is nice, but cannot instantiate unknowns in the assumptions *)
fun hyp_resolve_tac i st = let
--- a/src/HOL/Tools/cnf_funcs.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Jul 30 12:20:43 2009 +0200
@@ -517,7 +517,7 @@
fun cnf_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let
val thy = ProofContext.theory_of ctxt
val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
@@ -540,7 +540,7 @@
fun cnfx_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let
val thy = ProofContext.theory_of ctxt;
val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
--- a/src/HOL/Tools/meson.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jul 30 12:20:43 2009 +0200
@@ -586,9 +586,9 @@
SELECT_GOAL
(EVERY [ObjectLogic.atomize_prems_tac 1,
rtac ccontr 1,
- FOCUS (fn {context = ctxt', prems = negs, ...} =>
+ Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
EVERY1 [skolemize_prems_tac ctxt negs,
- FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
+ Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
(** Best-first search versions **)
--- a/src/HOL/Tools/record.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Tools/record.ML Thu Jul 30 12:20:43 2009 +0200
@@ -2161,7 +2161,7 @@
fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
- THEN (FOCUS (fn {prems, ...} => equality_tac prems) context 1))
+ THEN (Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1))
(* simp_all_tac ss (sel_convs) would also work but is less efficient *)
end);
val equality = timeit_msg "record equality proof:" equality_prf;
--- a/src/HOL/Tools/res_axioms.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Thu Jul 30 12:20:43 2009 +0200
@@ -517,7 +517,7 @@
SUBGOAL (fn (prop, i) =>
let val ts = Logic.strip_assums_hyp prop in
EVERY'
- [FOCUS
+ [Subgoal.FOCUS
(fn {prems, ...} =>
(Method.insert_tac
(map forall_intr_vars (neg_clausify prems)) i)) ctxt,
--- a/src/HOL/Tools/sat_funcs.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Thu Jul 30 12:20:43 2009 +0200
@@ -411,7 +411,7 @@
(* ------------------------------------------------------------------------- *)
fun rawsat_tac ctxt i =
- FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
+ Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jul 30 12:20:43 2009 +0200
@@ -788,7 +788,7 @@
all_tac) THEN
PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
(* use theorems generated from the actual justifications *)
- FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
+ Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
in
(* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
--- a/src/Provers/order.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Provers/order.ML Thu Jul 30 12:20:43 2009 +0200
@@ -1235,12 +1235,12 @@
val prfs = gen_solve mkconcl thy (lesss, C);
val (subgoals, prf) = mkconcl decomp less_thms thy C;
in
- FOCUS (fn {prems = asms, ...} =>
+ Subgoal.FOCUS (fn {prems = asms, ...} =>
let val thms = map (prove (prems @ asms)) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
handle Contr p =>
- (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
+ (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
handle Subscript => Seq.empty)
| Cannot => Seq.empty
| Subscript => Seq.empty)
--- a/src/Provers/quasi.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Provers/quasi.ML Thu Jul 30 12:20:43 2009 +0200
@@ -560,11 +560,11 @@
val (subgoal, prf) = mkconcl_trans thy C;
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
- handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
| Cannot => Seq.empty);
@@ -580,12 +580,12 @@
val prfs = solveQuasiOrder thy (lesss, C);
val (subgoals, prf) = mkconcl_quasi thy C;
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
handle Contr p =>
- (FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
handle Subscript => Seq.empty)
| Cannot => Seq.empty
| Subscript => Seq.empty);
--- a/src/Provers/trancl.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Provers/trancl.ML Thu Jul 30 12:20:43 2009 +0200
@@ -541,7 +541,7 @@
val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
val prfs = solveTrancl (prems, C);
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove thy rel prems) prfs
in rtac (prove thy rel thms prf) 1 end) ctxt n st
end
@@ -558,7 +558,7 @@
val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
val prfs = solveRtrancl (prems, C);
in
- FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove thy rel prems) prfs
in rtac (prove thy rel thms prf) 1 end) ctxt n st
end
--- a/src/Pure/subgoal.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Pure/subgoal.ML Thu Jul 30 12:20:43 2009 +0200
@@ -133,8 +133,5 @@
end;
-val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
-val FOCUS_PREMS = Subgoal.FOCUS_PREMS;
-val FOCUS = Subgoal.FOCUS;
val SUBPROOF = Subgoal.SUBPROOF;