equal
deleted
inserted
replaced
54 val (constr, cargs_frees) = |
54 val (constr, cargs_frees) = |
55 if null middle then raise RecError "constructor missing" |
55 if null middle then raise RecError "constructor missing" |
56 else strip_comb (hd middle); |
56 else strip_comb (hd middle); |
57 val (cname, _) = dest_Const constr |
57 val (cname, _) = dest_Const constr |
58 handle TERM _ => raise RecError "ill-formed constructor"; |
58 handle TERM _ => raise RecError "ill-formed constructor"; |
59 val con_info = the (Symtab.curried_lookup (ConstructorsData.get thy) cname) |
59 val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) |
60 handle Option => |
60 handle Option => |
61 raise RecError "cannot determine datatype associated with function" |
61 raise RecError "cannot determine datatype associated with function" |
62 |
62 |
63 val (ls, cargs, rs) = (map dest_Free ls_frees, |
63 val (ls, cargs, rs) = (map dest_Free ls_frees, |
64 map dest_Free cargs_frees, |
64 map dest_Free cargs_frees, |