equal
deleted
inserted
replaced
124 Type(ty_str, _) => ty_str |
124 Type(ty_str, _) => ty_str |
125 | TFree(s,_) => raise ERROR_MESSAGE |
125 | TFree(s,_) => raise ERROR_MESSAGE |
126 ("Free type: " ^ s) |
126 ("Free type: " ^ s) |
127 | TVar((s,i),_) => raise ERROR_MESSAGE |
127 | TVar((s,i),_) => raise ERROR_MESSAGE |
128 ("Free variable: " ^ s) |
128 ("Free variable: " ^ s) |
129 val dt = case Symtab.curried_lookup dtypestab ty_str |
129 val dt = case Symtab.lookup dtypestab ty_str |
130 of SOME dt => dt |
130 of SOME dt => dt |
131 | NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str) |
131 | NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str) |
132 in |
132 in |
133 cases_thm_of_induct_thm (#induction dt) |
133 cases_thm_of_induct_thm (#induction dt) |
134 end; |
134 end; |