# HG changeset patch
# User wenzelm
# Date 953141621 -3600
# Node ID f7b06595d0c8666df4b75da850999410fd17ee91
# Parent  df6549f5a01f2bbe4cf2e78dc2b1936bcc3cd627
removed export_chain;

diff -r df6549f5a01f -r f7b06595d0c8 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Mar 15 18:32:41 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 15 18:33:41 2000 +0100
@@ -74,7 +74,6 @@
   val with_facts_i: (thm * Proof.context attribute list) list * Comment.text
     -> ProofHistory.T -> ProofHistory.T
   val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
-  val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T
   val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
@@ -281,7 +280,6 @@
 val with_facts_i = gen_from_facts (gen_have_thmss_i add_thmss) o Comment.ignore;
 
 fun chain comment_ignore = ProofHistory.apply Proof.chain;
-fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain;
 
 
 (* context *)