changeset 32727 | 9072201cd69d |
parent 32712 | ec5976f4d3d8 |
child 32952 | aeb1e44fbc19 |
--- a/src/HOL/Tools/TFL/casesplit.ML Mon Sep 28 09:47:32 2009 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Mon Sep 28 10:20:21 2009 +0200 @@ -96,7 +96,7 @@ | TVar((s,i),_) => error ("Free variable: " ^ s) val dt = Datatype.the_info thy ty_str in - cases_thm_of_induct_thm (snd (#inducts dt)) + cases_thm_of_induct_thm (#induct dt) end; (*