src/Pure/Isar/isar_thy.ML
changeset 8466 f7b06595d0c8
parent 8450 dc44d6533f0f
child 8562 ce0e2b8e8844
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Mar 15 18:32:41 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 15 18:33:41 2000 +0100
     1.3 @@ -74,7 +74,6 @@
     1.4    val with_facts_i: (thm * Proof.context attribute list) list * Comment.text
     1.5      -> ProofHistory.T -> ProofHistory.T
     1.6    val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.7 -  val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.8    val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     1.9    val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.10    val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.11 @@ -281,7 +280,6 @@
    1.12  val with_facts_i = gen_from_facts (gen_have_thmss_i add_thmss) o Comment.ignore;
    1.13  
    1.14  fun chain comment_ignore = ProofHistory.apply Proof.chain;
    1.15 -fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain;
    1.16  
    1.17  
    1.18  (* context *)