equal
deleted
inserted
replaced
66 fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = |
66 fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = |
67 let |
67 let |
68 fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else (); |
68 fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else (); |
69 |
69 |
70 val typof = curry fastype_of1 bound_Ts; |
70 val typof = curry fastype_of1 bound_Ts; |
71 val build_map_fst = build_map ctxt (fst_const o fst); |
71 val build_map_fst = build_map ctxt [] (fst_const o fst); |
72 |
72 |
73 val yT = typof y; |
73 val yT = typof y; |
74 val yU = typof y'; |
74 val yU = typof y'; |
75 |
75 |
76 fun y_of_y' () = build_map_fst (yU, yT) $ y'; |
76 fun y_of_y' () = build_map_fst (yU, yT) $ y'; |