558 if Pattern.matches thy (rtrm', rtrm) |
558 if Pattern.matches thy (rtrm', rtrm) |
559 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
559 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
560 end |
560 end |
561 end |
561 end |
562 |
562 |
563 | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
563 | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
564 ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
564 ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
565 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) |
565 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) |
566 |
566 |
567 | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)), |
567 | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)), |
568 ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) => |
568 ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) => |
569 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) |
569 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) |
570 |
570 |
571 | (t1 $ t2, t1' $ t2') => |
571 | (t1 $ t2, t1' $ t2') => |
572 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
572 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
573 |
573 |