src/Pure/Isar/proof.ML

 fun export_facts inner outer =
   (case get_facts inner of
     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));
 
 
 (* mode *)
 

     (Tactic.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
       if can Logic.unprotect (Logic.strip_assums_concl goal) then
         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
+in
+
+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 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);
+    |> Seq.maps (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
+  end;
 
 end;
 
 
 (* conclude_goal *)

     val outer_state = state |> close_block;
     val outer_ctxt = context_of outer_state;
 
     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)
     |> pair (after_qed, results)
   end;

       #> Sign.restore_naming thy;
 
     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
     |> generic_goal (prepp #> ProofContext.auto_fixes) (kind ^ goal_names target name names)
       before_qed (K Seq.single, after_qed') propp