equal
deleted
inserted
replaced
120 if i > 0 then trans_pat i T fresh_term ([], v) |
120 if i > 0 then trans_pat i T fresh_term ([], v) |
121 else trans_expr T v #>> pair [] |
121 else trans_expr T v #>> pair [] |
122 | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v) |
122 | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v) |
123 |
123 |
124 fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u) |
124 fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u) |
125 fun mk_eq (Const (@{const_name apply}, _)) (u' :: us', u) = mk_eq' u' us' u |
125 fun mk_eq (Const (@{const_name fun_app}, _)) (u' :: us', u) = mk_eq' u' us' u |
126 | mk_eq t (us, u) = mk_eq' t us u |
126 | mk_eq t (us, u) = mk_eq' t us u |
127 |
127 |
128 fun translate (t, cs) = |
128 fun translate (t, cs) = |
129 let val T = Term.fastype_of t |
129 let val T = Term.fastype_of t |
130 in |
130 in |