# HG changeset patch
# User wenzelm
# Date 1129911293 -7200
# Node ID ef2c44da2f685ea59d415c608e039547fbc0c8f8
# Parent  4969d6eb4c97c499436814ecf00fc7b02d9186d2
Goal.prove_plain;

diff -r 4969d6eb4c97 -r ef2c44da2f68 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Oct 21 18:14:52 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Oct 21 18:14:53 2005 +0200
@@ -1907,7 +1907,7 @@
 
     val cert = Thm.cterm_of defs_thy;
 
-    val intro = Drule.standard (Tactic.prove defs_thy [] norm_ts statement (fn _ =>
+    val intro = Drule.standard (Goal.prove defs_thy [] norm_ts statement (fn _ =>
       Tactic.rewrite_goals_tac [pred_def] THEN
       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
       Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
@@ -1917,7 +1917,7 @@
         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Drule.conj_elim_precise (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
-      Tactic.prove_plain defs_thy [] [] t (fn _ =>
+      Goal.prove_plain defs_thy [] [] t (fn _ =>
         Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in (defs_thy, (statement, intro, axioms)) end;