Replaced datatype_info by datatype_info_err.
authorberghofe
Fri, 16 Jul 1999 13:25:45 +0200
changeset 7017 e4e64a0b0b6b
parent 7016 df54b5365477
child 7018 ae18bb3075c3
Replaced datatype_info by datatype_info_err.
src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Fri Jul 16 13:24:41 1999 +0200
+++ b/src/HOL/Tools/induct_method.ML	Fri Jul 16 13:25:45 1999 +0200
@@ -29,7 +29,7 @@
 
 (* induct_rule *)
 
-fun kind_rule Type = (#induction oo DatatypePackage.datatype_info, Sign.intern_tycon)
+fun kind_rule Type = (#induction oo DatatypePackage.datatype_info_err, Sign.intern_tycon)
   | kind_rule Set = ((#induct o #2) oo InductivePackage.get_inductive, Sign.intern_const)
   | kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const);