378 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
378 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
379 | _ => f (trm1, trm2) |
379 | _ => f (trm1, trm2) |
380 |
380 |
381 fun relation_error ctxt r1 r2 = |
381 fun relation_error ctxt r1 r2 = |
382 let |
382 let |
383 val r1s = Syntax.string_of_term ctxt r1 |
383 val r1_str = Syntax.string_of_term ctxt r1 |
384 val r2s = Syntax.string_of_term ctxt r2 |
384 val r2_str = Syntax.string_of_term ctxt r2 |
385 val r1t = Syntax.string_of_typ ctxt (fastype_of r1) |
385 val r1_ty_str = Syntax.string_of_typ ctxt (fastype_of r1) |
386 val r2t = Syntax.string_of_typ ctxt (fastype_of r2) |
386 val r2_ty_str = Syntax.string_of_typ ctxt (fastype_of r2) |
387 in |
387 in |
388 raise LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
388 raise LIFT_MATCH |
389 r1s ^ " :: " ^ r1t ^ "]\n[" ^ r2s ^ " :: " ^ r2t ^ "]") |
389 (cat_lines ["regularise (relation mismatch)", r1_str ^ "::" ^ r1_ty_str, r2_str ^ "::" ^ r2_ty_str]) |
390 end |
390 end |
391 |
391 |
392 (* the major type of All and Ex quantifiers *) |
392 (* the major type of All and Ex quantifiers *) |
393 fun qnt_typ ty = domain_type (domain_type ty) |
393 fun qnt_typ ty = domain_type (domain_type ty) |
394 |
394 |