# HG changeset patch
# User wenzelm
# Date 1152356087 -7200
# Node ID 25935807eb082f597c06d1f668fc7a01b38e0f88
# Parent  7d035e26e5f9ed41cc0c830a8d6e875e4d705dd3
Element.prove_witness: context;
Goal.prove_global;

diff -r 7d035e26e5f9 -r 25935807eb08 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jul 08 12:54:46 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jul 08 12:54:47 2006 +0200
@@ -1644,20 +1644,21 @@
         Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
       |> Theory.add_consts_i [(bname, predT, NoSyn)]
       |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
+    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;
 
-    val intro = Drule.standard (Goal.prove defs_thy [] norm_ts statement (fn _ =>
+    val intro = Goal.prove_global 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, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
+      Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq,
         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_precise [length ts] |> hd;
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
-      Element.prove_witness defs_thy t
+      Element.prove_witness defs_ctxt t
        (Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;