# HG changeset patch
# User wenzelm
# Date 1008718107 -3600
# Node ID 65f03a3f7998ff55ebbd19724f1ae9fd8814cb00
# Parent  9d247ad51c813ecfb4b321edbfa64fc9620ba8f7
tuned interface of ProofContext.generalize;
tuned;

diff -r 9d247ad51c81 -r 65f03a3f7998 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Dec 19 00:26:39 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Dec 19 00:28:27 2001 +0100
@@ -651,12 +651,13 @@
 (*global goals*)
 fun global_goal prep kind a raw_locale elems args thy =
   let
-    val st = thy |> init_state |> open_block;
+    val init = init_state thy;
     val (opt_name, locale_ctxt, elems_ctxt, propp) =
-      prep (apsome fst raw_locale) elems (map snd args) (context_of st);
+      prep (apsome fst raw_locale) elems (map snd args) (context_of init);
     val locale = (case raw_locale of None => None | Some (_, atts) => Some (the opt_name, atts));
   in
-    st
+    init
+    |> open_block
     |> map_context (K locale_ctxt)
     |> open_block
     |> map_context (K elems_ctxt)
@@ -744,7 +745,7 @@
   in
     print_result goal_ctxt (kind_name (sign_of state) kind, names ~~ Library.unflat tss results);
     outer_state
-    |> auto_bind_facts (map (ProofContext.generalize goal_ctxt outer_ctxt) ts)
+    |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
     |> (fn st => Seq.map (fn res =>
       have_thmss ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
     |> (Seq.flat o Seq.map opt_solve)