# HG changeset patch
# User wenzelm
# Date 1008365351 -3600
# Node ID 901c6c4779076f78caf4ad396541958f8ef9db86
# Parent  172d18ec3b549c7ebfb1d5cee05e63e5afd00981
tuned locale interface;

diff -r 172d18ec3b54 -r 901c6c477907 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Dec 14 22:28:52 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Dec 14 22:29:11 2001 +0100
@@ -652,14 +652,14 @@
 fun global_goal prepp prep_locale activate kind a raw_locale elems args thy =
   let
     val st = thy |> init_state |> open_block;
-    val (activate_locale, activate_elems) = activate (context_of st)
+    val (locale_ctxt, elems_ctxt) = context_of st |> activate
       ((case raw_locale of None => Locale.empty | Some (name, _) => Locale.Locale name), elems);
     val locale = apsome (apfst (prep_locale (Theory.sign_of thy))) raw_locale;
   in
     st
-    |> map_context activate_locale
+    |> map_context (K locale_ctxt)
     |> open_block
-    |> map_context activate_elems
+    |> map_context (K elems_ctxt)
     |> setup_goal I prepp ProofContext.fix_frees (Theorem (kind, a, locale, map (snd o fst) args))
       Seq.single (map (fst o fst) args) (map snd args)
   end;