src/HOL/Tools/TFL/casesplit.ML
changeset 31723 f5cafe803b55
parent 29270 0eade173f77e
child 31784 bd3486c57ba3
equal deleted inserted replaced
31717:d1f7b6245a75 31723:f5cafe803b55
    88      Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
    88      Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
    89 
    89 
    90 (* get the case_thm (my version) from a type *)
    90 (* get the case_thm (my version) from a type *)
    91 fun case_thm_of_ty sgn ty  =
    91 fun case_thm_of_ty sgn ty  =
    92     let
    92     let
    93       val dtypestab = DatatypePackage.get_datatypes sgn;
    93       val dtypestab = Datatype.get_datatypes sgn;
    94       val ty_str = case ty of
    94       val ty_str = case ty of
    95                      Type(ty_str, _) => ty_str
    95                      Type(ty_str, _) => ty_str
    96                    | TFree(s,_)  => error ("Free type: " ^ s)
    96                    | TFree(s,_)  => error ("Free type: " ^ s)
    97                    | TVar((s,i),_) => error ("Free variable: " ^ s)
    97                    | TVar((s,i),_) => error ("Free variable: " ^ s)
    98       val dt = case Symtab.lookup dtypestab ty_str
    98       val dt = case Symtab.lookup dtypestab ty_str