src/Pure/Isar/isar_thy.ML
changeset 7666 226ea33c7cd6
parent 7633 838077e40a46
child 7678 027b6ec2f084
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Sep 30 21:21:52 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Sep 30 21:22:26 1999 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4    val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.5    val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.6    val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     1.7 -  val fix_i: ((string list * typ) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     1.8 +  val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     1.9    val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.10    val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.11    val theorem: (bstring * Args.src list * (string * (string list * string list)))
    1.12 @@ -93,7 +93,7 @@
    1.13      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.14    val local_def: (string * Args.src list * ((string * string option) * (string * string list)))
    1.15      * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.16 -  val local_def_i: (string * Args.src list * ((string * typ) * (term * term list)))
    1.17 +  val local_def_i: (string * Args.src list * ((string * typ option) * (term * term list)))
    1.18      * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.19    val show: (string * Args.src list * (string * (string list * string list)))
    1.20      * Comment.text -> ProofHistory.T -> ProofHistory.T