equal
deleted
inserted
replaced
95 apfst (curry list_all_free frees) (mk_prems (map Free frees) recs)) |
95 apfst (curry list_all_free frees) (mk_prems (map Free frees) recs)) |
96 end) (j, constrs)) (1, descr ~~ recTs)))); |
96 end) (j, constrs)) (1, descr ~~ recTs)))); |
97 |
97 |
98 fun mk_proj j [] t = t |
98 fun mk_proj j [] t = t |
99 | mk_proj j (i :: is) t = if null is then t else |
99 | mk_proj j (i :: is) t = if null is then t else |
100 if j = i then HOLogic.mk_fst t |
100 if (j: int) = i then HOLogic.mk_fst t |
101 else mk_proj j is (HOLogic.mk_snd t); |
101 else mk_proj j is (HOLogic.mk_snd t); |
102 |
102 |
103 val tnames = DatatypeProp.make_tnames recTs; |
103 val tnames = DatatypeProp.make_tnames recTs; |
104 val fTs = map fastype_of rec_fns; |
104 val fTs = map fastype_of rec_fns; |
105 val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T |
105 val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T |