# HG changeset patch # User Cezary Kaliszyk # Date 1264591300 -3600 # Node ID d7ec7b1204a542b3d71fde486c0b7c07af7f40ea # Parent 1786aa86e52bceb0a260a117a4970a05d35090cc# Parent fd2493ae3df2321fd66d075d324353ffd1cb9bbc merge diff -r fd2493ae3df2 -r d7ec7b1204a5 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Wed Jan 27 12:19:21 2010 +0100 +++ b/Quot/quotient_term.ML Wed Jan 27 12:21:40 2010 +0100 @@ -370,9 +370,9 @@ but also accepts partially regularized terms. This means that the raw theorems can have: - Ball (Respects R), Bex (Respects R), Bexeq (Respects R), R + Ball (Respects R), Bex (Respects R), Bexeq (Respects R), Babs, R in the places where: - All, Ex, Ex1, (op =) + All, Ex, Ex1, %, (op =) is required the lifted theorem. *) @@ -439,6 +439,15 @@ if ty = ty' then subtrm else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm end + | (Const (@{const_name "Babs"}, T) $ r $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => + let + val subtrm = regularize_trm ctxt (t, t') + val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') + in + if r <> needres + then term_mismatch "regularize (Babs)" ctxt r needres + else mk_babs $ r $ subtrm + end | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => let