--- a/QuotMain.thy	Tue Oct 13 11:03:55 2009 +0200
+++ b/QuotMain.thy	Tue Oct 13 11:38:35 2009 +0200
@@ -321,11 +321,12 @@
 *}
 
 definition
-  "x IN p ==> (Babs p m x = m x)"
+  "(x : p) ==> (Babs p m x = m x)"
 
 print_theorems
 thm Babs_def
 ML {* type_of @{term Babs } *}
+ML {* type_of @{term Ball } *}
 ML {*
   cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
 *}
@@ -347,7 +348,7 @@
         val res_term = respects $ sub_res_term;
         val ty = fastype_of trm;
         val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
-        val rabs_term = rabs $ respects $ lam_term;
+        val rabs_term = (rabs $ respects) $ lam_term;
       in
         rabs_term
       end else let
@@ -362,6 +363,15 @@
 
 *}
 
+term "Babs (Respects (RR)) (\<lambda>x :: trm. x)"
+
+(*
+ML {*
+  Toplevel.program (fn () =>
+  cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context})
+  )
+*}
+
 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
   trm == new_trm
 *)