--- a/QuotMain.thy	Mon Dec 07 11:14:21 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 12:14:25 2009 +0100
@@ -172,13 +172,6 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
-section {* Bounded abstraction *}
-
-definition
-  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
-  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-
 section {* Simset setup *}
 
 (* since HOL_basic_ss is too "big", we need to set up *)
@@ -418,10 +411,10 @@
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (x', ty', t')) =>
        let
-         val subtrm = regularize_trm lthy t t'
-       in     
+         val subtrm = Abs(x, ty, regularize_trm lthy t t')
+       in
          if ty = ty'
-         then Abs (x, ty, subtrm)
+         then subtrm
          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
        end