equal
deleted
inserted
replaced
982 fun qtn (Type(a,tl)) = (a,tl) | |
982 fun qtn (Type(a,tl)) = (a,tl) | |
983 qtn _ = error "unexpected type variable in preprocess_td"; |
983 qtn _ = error "unexpected type variable in preprocess_td"; |
984 val s = post_last_dot(fst(qtn a)); |
984 val s = post_last_dot(fst(qtn a)); |
985 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t | |
985 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t | |
986 param_types _ = error "malformed induct-theorem in preprocess_td"; |
986 param_types _ = error "malformed induct-theorem in preprocess_td"; |
987 val pl = param_types (concl_of (get_thm sg (s ^ ".induct", NONE))); |
987 val pl = param_types (concl_of (get_thm sg (Name (s ^ ".induct")))); |
988 val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (s ^ ".induct", NONE))); |
988 val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (Name (s ^ ".induct")))); |
989 val ntl = new_types l; |
989 val ntl = new_types l; |
990 in |
990 in |
991 ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done))) |
991 ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done))) |
992 end) |
992 end) |
993 end; |
993 end; |