src/Pure/Isar/proof_context.ML

   val declare_terms: term list -> context -> context
   val warn_extra_tfrees: context -> context -> context
   val generalize: context -> context -> term list -> term list
   val find_free: term -> string -> term option
   val export: bool -> context -> context -> thm -> thm Seq.seq
-  val export_standard: cterm option -> context -> context -> thm -> thm
+  val export_standard: cterm list -> context -> context -> thm -> thm
   val drop_schematic: indexname * term option -> indexname * term option
   val add_binds: (indexname * string option) list -> context -> context
   val add_binds_i: (indexname * term option) list -> context -> context
   val auto_bind_goal: term list -> context -> context
   val auto_bind_facts: term list -> context -> context

 fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None
   | get_free _ (opt, _) = opt;
 
 fun find_free t x = foldl_aterms (get_free x) (None, t);
 
-fun export0 view is_goal inner outer =
+fun export_view view is_goal inner outer =
   let
     val gen = generalize_tfrees inner outer;
     val fixes = fixed_names_of inner \\ fixed_names_of outer;
     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   in fn thm => thm
     |> Tactic.norm_hhf_rule
     |> Seq.EVERY (rev exp_asms)
-    |> Seq.map (case view of None => I | Some A => Thm.implies_intr A)
+    |> Seq.map (Drule.implies_intr_list view)
     |> Seq.map (fn rule =>
       let
         val {sign, prop, ...} = Thm.rep_thm rule;
         val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
         val tfrees = gen (Term.add_term_tfree_names (prop, []));

         |> Tactic.norm_hhf_rule
         |> (#1 o Drule.tvars_intr_list tfrees)
       end)
   end;
 
-val export = export0 None;
+val export = export_view [];
 
 fun export_standard view inner outer =
-  let val exp = export0 view false inner outer in
+  let val exp = export_view view false inner outer in
     fn th =>
       (case Seq.pull (exp th) of
         Some (th', _) => th' |> Drule.local_standard
       | None => raise CONTEXT ("Internal failure while exporting theorem", inner))
   end;