src/HOL/Tools/recdef_package.ML
changeset 12708 31672377dadc
parent 12694 9950c1ce9d24
child 12755 a906a8b364f1
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jan 11 00:27:40 2002 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Jan 11 00:28:24 2002 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4      theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
     1.5    val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
     1.6      -> theory -> theory * {induct_rules: thm}
     1.7 -  val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
     1.8 +  val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
     1.9      -> theory -> theory * {induct_rules: thm}
    1.10    val recdef_tc: bstring * Args.src list -> xstring -> int option
    1.11      -> bool -> theory -> ProofHistory.T