src/HOL/Tools/TFL/casesplit.ML
changeset 32727 9072201cd69d
parent 32712 ec5976f4d3d8
child 32952 aeb1e44fbc19
equal deleted inserted replaced
32723:866cebde3fca 32727:9072201cd69d
    94                      Type(ty_str, _) => ty_str
    94                      Type(ty_str, _) => ty_str
    95                    | TFree(s,_)  => error ("Free type: " ^ s)
    95                    | TFree(s,_)  => error ("Free type: " ^ s)
    96                    | TVar((s,i),_) => error ("Free variable: " ^ s)
    96                    | TVar((s,i),_) => error ("Free variable: " ^ s)
    97       val dt = Datatype.the_info thy ty_str
    97       val dt = Datatype.the_info thy ty_str
    98     in
    98     in
    99       cases_thm_of_induct_thm (snd (#inducts dt))
    99       cases_thm_of_induct_thm (#induct dt)
   100     end;
   100     end;
   101 
   101 
   102 (*
   102 (*
   103  val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
   103  val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
   104 *)
   104 *)