# HG changeset patch
# User wenzelm
# Date 1129911274 -7200
# Node ID 369e2af8ee458b3bfa7238806f135c85704b4342
# Parent  3b34516662c642302c0de4744939bcce59a88c51
Goal.prove;

diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Algebra/abstract/Ring.thy
--- a/src/HOL/Algebra/abstract/Ring.thy	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy	Fri Oct 21 18:14:34 2005 +0200
@@ -164,7 +164,7 @@
 	 "t * u::'a::ring",
 	 "- t::'a::ring"];
     fun proc sg ss t = 
-      let val rew = Tactic.prove sg [] []
+      let val rew = Goal.prove sg [] []
             (HOLogic.mk_Trueprop
               (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
                 (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Fun.thy	Fri Oct 21 18:14:34 2005 +0200
@@ -497,7 +497,7 @@
       (fn sg => fn ss => fn t =>
         case find_double t of (T, NONE) => NONE
         | (T, SOME rhs) =>
-            SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
+            SOME (Goal.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
 end;
 Addsimprocs[fun_upd2_simproc];
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Hoare/hoare.ML
--- a/src/HOL/Hoare/hoare.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hoare/hoare.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -82,7 +82,7 @@
                            Free ("P",varsT --> boolT) $ Bound 0));
                    val impl = implies $ (Mset_incl big_Collect) $ 
                                           (Mset_incl small_Collect);
-   in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Hoare/hoareAbort.ML
--- a/src/HOL/Hoare/hoareAbort.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -83,7 +83,7 @@
                            Free ("P",varsT --> boolT) $ Bound 0));
                    val impl = implies $ (Mset_incl big_Collect) $ 
                                           (Mset_incl small_Collect);
-   in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -72,7 +72,7 @@
       , REPEAT_ALL_NEW (resolve_tac intros) 1
       , match_tac [reflexive_thm] 1 ]
   in
-    prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
+    OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
   end
 
 fun transfer_tac ths =
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/IMPP/Hoare.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -268,7 +268,7 @@
 by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
 by  (Fast_tac 1);
 by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
-byev[dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3];
+by (EVERY [dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]);
 by   (eresolve_tac (tl(tl(tl(premises())))) 3);
 by   (Fast_tac 1);
 by (dtac finite_subset 1);
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -96,7 +96,7 @@
     if t aconv u then NONE
     else
       let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
-      in SOME (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
+      in SOME (Goal.prove sg xs [] eq (K (EVERY tacs))) end
 
   fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
   fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/List.thy	Fri Oct 21 18:14:34 2005 +0200
@@ -453,7 +453,7 @@
         val app = Const("List.op @",appT)
         val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
-        val thm = Tactic.prove sg [] [] eq
+        val thm = Goal.prove sg [] [] eq
           (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
       in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Product_Type.thy	Fri Oct 21 18:14:34 2005 +0200
@@ -413,7 +413,7 @@
   fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
   |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
   |   split_pat tp i _ = NONE;
-  fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
+  fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] []
         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
         (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -347,10 +347,10 @@
                              in (case (#distinct (datatype_info_err sg tname1)) of
                                  QuickAndDirty => SOME (Thm.invoke_oracle
                                    Datatype_thy distinctN (sg, ConstrDistinct eq_t))
-                               | FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
+                               | FewConstrs thms => SOME (Goal.prove sg [] [] eq_t (K
                                    (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
                                     atac 2, resolve_tac thms 1, etac FalseE 1])))
-                               | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
+                               | ManyConstrs (thm, simpset) => SOME (Goal.prove sg [] [] eq_t (K
                                    (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
                                     full_simp_tac (Simplifier.inherit_context ss simpset) 1,
                                     REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -226,8 +226,8 @@
     val (cset, goal, _, typedef_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
     val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
-    val non_empty = Tactic.prove thy [] [] goal (K tac) handle ERROR =>
-      error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
+    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR_MESSAGE msg =>
+      error (msg ^ "\nFailed to prove non-emptiness of " ^ quote (string_of_cterm cset));
     val ((thy', _), result) = (thy, non_empty) |> typedef_result;
   in (thy', result) end;
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/HOLCF/adm_tac.ML
--- a/src/HOLCF/adm_tac.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOLCF/adm_tac.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -102,7 +102,7 @@
          | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
        val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
        val t' = mk_all params (Logic.list_implies (prems, t));
-       val thm = Tactic.prove sign [] [] t' (K (tac 1));
+       val thm = Goal.prove sign [] [] t' (K (tac 1));
   in (ts, thm)::l end
   handle ERROR_MESSAGE _ => l;
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -90,7 +90,7 @@
 
 fun sum_proc sg ss t =
    let val t' = cancel sg t
-       val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
+       val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
                    (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
    in SOME thm end
    handle Cancel => NONE;
@@ -110,7 +110,7 @@
 
  fun rel_proc sg ss t =
    let val t' = cancel sg t
-       val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
+       val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
                    (fn _ => rtac eq_reflection 1 THEN
                             resolve_tac eqI_rules 1 THEN
                             simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
diff -r 3b34516662c6 -r 369e2af8ee45 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/Arith/assoc_fold.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -54,7 +54,7 @@
                else ()
        val rhs = plus $ mk_sum plus lits $ mk_sum plus others
        val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
-       val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
+       val th = Goal.prove thy [] [] (Logic.mk_equals (lhs, rhs))
                    (fn _ => rtac Data.eq_reflection 1 THEN
                             simp_tac (Simplifier.inherit_context ss assoc_ss) 1)
    in SOME th end
diff -r 3b34516662c6 -r 369e2af8ee45 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/quantifier1.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -104,7 +104,7 @@
   in exqu end;
 
 fun prove_conv tac thy tu =
-  Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
+  Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
 
diff -r 3b34516662c6 -r 369e2af8ee45 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -35,7 +35,7 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove thy xs asms prop tac =
-  Tactic.prove thy xs asms prop
+  Goal.prove thy xs asms prop
     (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
 
 end;
diff -r 3b34516662c6 -r 369e2af8ee45 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Pure/axclass.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -272,8 +272,8 @@
     val (c1, c2) = prep_classrel thy raw_cc;
     val txt = quote (Sign.string_of_classrel thy [c1, c2]);
     val _ = message ("Proving class inclusion " ^ txt ^ " ...");
-    val th = Tactic.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
-      error ("The error(s) above occurred while trying to prove " ^ txt);
+    val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg =>
+      error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   in add_classrel_thms [th] thy end;
 
 fun ext_inst_arity prep_arity raw_arity tac thy =
@@ -282,9 +282,9 @@
     val txt = quote (Sign.string_of_arity thy arity);
     val _ = message ("Proving type arity " ^ txt ^ " ...");
     val props = (mk_arities arity);
-    val ths = Tactic.prove_multi thy [] [] props
-        (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
-      handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
+    val ths = Goal.prove_multi thy [] [] props
+      (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) handle ERROR_MESSAGE msg =>
+        error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   in add_arity_thms ths thy end;
 
 in
diff -r 3b34516662c6 -r 369e2af8ee45 src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/ZF/Datatype.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -87,7 +87,7 @@
                  writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
                else ();
        val goal = Logic.mk_equals (old, new)
-       val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
+       val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
            simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
          handle ERROR_MESSAGE msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
diff -r 3b34516662c6 -r 369e2af8ee45 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/ZF/arith_data.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -74,7 +74,7 @@
   let val hyps' = List.filter (not o is_eq_thm) hyps
       val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
         FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
-  in SOME (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))
+  in SOME (hyps' MRS Goal.prove sg xs [] goal (K (EVERY tacs)))
       handle ERROR_MESSAGE msg =>
         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
   end;