# HG changeset patch
# User wenzelm
# Date 1248949243 -7200
# Node ID 3bebc195c124e91ce9fc5b9719efc989e3813709
# Parent  853ef99c04cc5a6109fb0a5655e1b890be004ddc
qualified Subgoal.FOCUS;

diff -r 853ef99c04cc -r 3bebc195c124 src/CCL/Wfd.thy
--- 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 =
diff -r 853ef99c04cc -r 3bebc195c124 src/HOL/Decision_Procs/Approximation.thy
--- 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
diff -r 853ef99c04cc -r 3bebc195c124 src/HOL/Prolog/prolog.ML
--- 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
diff -r 853ef99c04cc -r 3bebc195c124 src/HOL/Tools/cnf_funcs.ML
--- 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
diff -r 853ef99c04cc -r 3bebc195c124 src/HOL/Tools/meson.ML
--- 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 **)
diff -r 853ef99c04cc -r 3bebc195c124 src/HOL/Tools/record.ML
--- 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;
diff -r 853ef99c04cc -r 3bebc195c124 src/HOL/Tools/res_axioms.ML
--- 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,
diff -r 853ef99c04cc -r 3bebc195c124 src/HOL/Tools/sat_funcs.ML
--- 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                                    *)
diff -r 853ef99c04cc -r 3bebc195c124 src/Provers/Arith/fast_lin_arith.ML
--- 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
diff -r 853ef99c04cc -r 3bebc195c124 src/Provers/order.ML
--- 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)
diff -r 853ef99c04cc -r 3bebc195c124 src/Provers/quasi.ML
--- 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);
diff -r 853ef99c04cc -r 3bebc195c124 src/Provers/trancl.ML
--- 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
diff -r 853ef99c04cc -r 3bebc195c124 src/Pure/subgoal.ML
--- 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;