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