# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264591198 -3600
# Node ID 1786aa86e52bceb0a260a117a4970a05d35090cc
# Parent  921096706b84ee835018a76e4f05c82da096a714
When commenting discovered a missing case of Babs->Abs regularization.

diff -r 921096706b84 -r 1786aa86e52b Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 27 12:06:43 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 12:19:58 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