changeset 31784 | bd3486c57ba3 |
parent 31775 | 2b04504fcb69 |
child 32013 | 5589a5360ddc |
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 23 15:32:34 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 23 16:27:12 2009 +0200 @@ -217,7 +217,7 @@ if ! Proofterm.proofs < 2 then thy else let val _ = message config "Adding realizers for induction and case analysis ..." - val infos = map (Datatype.the_datatype thy) names; + val infos = map (Datatype.the_info thy) names; val info :: _ = infos; in thy