# HG changeset patch
# User wenzelm
# Date 1010675366 -3600
# Node ID 7bffaadc581e02c0294bd91f01550915af0fbc8f
# Parent  af5fec8a418f483396a729cd53bcf24621ab43a1
export_single;

diff -r af5fec8a418f -r 7bffaadc581e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jan 10 16:06:39 2002 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Jan 10 16:09:26 2002 +0100
@@ -48,6 +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 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
@@ -738,6 +739,11 @@
       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));
+
 
 
 (** bindings **)