equal
deleted
inserted
replaced
44 val (middle, rs_frees) = chop_suffix is_Free rest; |
44 val (middle, rs_frees) = chop_suffix is_Free rest; |
45 |
45 |
46 val (constr, cargs_frees) = |
46 val (constr, cargs_frees) = |
47 if null middle then raise RecError "constructor missing" |
47 if null middle then raise RecError "constructor missing" |
48 else strip_comb (hd middle); |
48 else strip_comb (hd middle); |
49 val (cname, _) = dest_Const constr |
49 val cname = dest_Const_name constr |
50 handle TERM _ => raise RecError "ill-formed constructor"; |
50 handle TERM _ => raise RecError "ill-formed constructor"; |
51 val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) |
51 val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) |
52 handle Option.Option => |
52 handle Option.Option => |
53 raise RecError "cannot determine datatype associated with function" |
53 raise RecError "cannot determine datatype associated with function" |
54 |
54 |
100 |
100 |
101 (*Replace X_rec(args,t) by fname(ls,t,rs) *) |
101 (*Replace X_rec(args,t) by fname(ls,t,rs) *) |
102 fun use_fabs (_ $ t) = subst_bound (t, fabs) |
102 fun use_fabs (_ $ t) = subst_bound (t, fabs) |
103 | use_fabs t = t |
103 | use_fabs t = t |
104 |
104 |
105 val cnames = map (#1 o dest_Const) constructors |
105 val cnames = map dest_Const_name constructors |
106 and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites |
106 and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites |
107 |
107 |
108 fun absterm (Free x, body) = absfree x body |
108 fun absterm (Free x, body) = absfree x body |
109 | absterm (t, body) = Abs("rec", \<^Type>\<open>i\<close>, abstract_over (t, body)) |
109 | absterm (t, body) = Abs("rec", \<^Type>\<open>i\<close>, abstract_over (t, body)) |
110 |
110 |