ProofContext.exports: simultaneous facts;
Variable.exportT_terms;

--- a/src/Pure/Isar/proof.ML	Sat Jun 17 19:37:55 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Jun 17 19:37:57 2006 +0200
@@ -230,7 +230,7 @@
     NONE => Seq.single (put_facts NONE outer)
   | SOME thms =>
       thms
-      |> Seq.map_list (ProofContext.exports (context_of inner) (context_of outer))
+      |> ProofContext.exports (context_of inner) (context_of outer)
       |> Seq.map (fn ths => put_facts (SOME ths) outer));
 
 
@@ -444,19 +444,17 @@
         Tactic.etac Drule.protectI i
       else all_tac)));
 
-fun refine_goal print_rule inner raw_rule state =
-  let val (outer, (_, goal)) = get_goal state in
-    raw_rule
-    |> ProofContext.goal_exports inner outer
-    |> Seq.maps (fn rule =>
-      (print_rule outer rule;
-        Seq.lift set_goal (FINDGOAL (refine_tac rule) goal) state))
-  end;
-
 in
 
-fun refine_goals print_rule inner raw_rules =
-  Seq.EVERY (map (refine_goal print_rule inner) raw_rules);
+fun refine_goals print_rule inner raw_rules state =
+  let
+    val (outer, (_, goal)) = get_goal state;
+    fun refine rule st = (print_rule outer rule; FINDGOAL (refine_tac rule) st);
+  in
+    raw_rules
+    |> ProofContext.goal_exports inner outer
+    |> Seq.maps (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
+  end;
 
 end;
 
@@ -827,10 +825,10 @@
 
     val props =
       flat (tl stmt)
-      |> Variable.generalize goal_ctxt outer_ctxt;
+      |> Variable.exportT_terms goal_ctxt outer_ctxt;
     val results =
       tl (conclude_goal state goal stmt)
-      |> (Seq.map_list o Seq.map_list) (ProofContext.exports goal_ctxt outer_ctxt);
+      |> Seq.map_list (ProofContext.exports goal_ctxt outer_ctxt);
   in
     outer_state
     |> map_context (ProofContext.auto_bind_facts props)
@@ -884,8 +882,8 @@
     fun after_qed' results =
       (case target of NONE => I
       | SOME prfx => store_results (NameSpace.base prfx)
-          (map (map (ProofContext.export_standard ctxt thy_ctxt
-            #> Drule.strip_shyps_warning)) results))
+          (map (ProofContext.export_standard ctxt thy_ctxt
+            #> map Drule.strip_shyps_warning) results))
       #> after_qed results;
   in
     init ctxt