--- 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 **)