# HG changeset patch
# User wenzelm
# Date 1026837727 -7200
# Node ID b261d9cdd6b2f39646863f3778b6d00cf42ff7be
# Parent  cc8245843abcebe7d22eb5b037247eaf89da1f3a
export_standard supercedes export_single;

diff -r cc8245843abc -r b261d9cdd6b2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 16 18:41:50 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 16 18:42:07 2002 +0200
@@ -48,7 +48,7 @@
   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_single: context -> context -> thm -> thm
+  val export_standard: 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
@@ -752,10 +752,13 @@
       end)
   end;
 
-fun export_single inner outer th =
-  (case Seq.pull (export false inner outer th) of
-    Some (th', _) => th'
-  | None => raise CONTEXT ("Internal failure while exporting theorem", inner));
+fun export_standard inner outer =
+  let val exp = export 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;
 
 
 
@@ -1397,7 +1400,7 @@
     val empty_idx = Library.null cs andalso Library.null xs;
 
     val header =
-      if empty_idx then [Pretty.block [Pretty.str "All known facts:", Pretty.fbrk]]
+      if empty_idx then [Pretty.block [Pretty.str "Known facts:", Pretty.fbrk]]
       else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" ::
         separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @
           [Pretty.str ":", Pretty.fbrk])]