--- a/Quot/Nominal/Test.thy	Wed Jan 27 14:06:17 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 14:06:34 2010 +0100
@@ -202,11 +202,11 @@
   bi::"bp \<Rightarrow> name set"
 where
   "bi (BP x t) = {x}"
-
+print_theorems
 
 text {* examples 2 *}
 nominal_datatype trm =
-  Var "string"
+  Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"        bindset x in t 
 | Let p::"pat" "trm" t::"trm"   bind "f p" in t
@@ -222,7 +222,7 @@
 | "f (PD (x,y)) = {x,y}"
 
 nominal_datatype trm2 =
-  Var2 "string"
+  Var2 "name"
 | App2 "trm2" "trm2"
 | Lam2 x::"name" t::"trm2"          bindset x in t 
 | Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
@@ -248,4 +248,4 @@
 
 
 
-end
\ No newline at end of file
+end

--- a/Quot/quotient_term.ML	Wed Jan 27 14:06:17 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 14:06:34 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