# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256024242 -7200
# Node ID 72d003e823491b1d8abcca5a76fc5da647ec497f
# Parent  5cdb383cef9c4f10fc3c81bd4adf333e2749c71b
some minor tuning

diff -r 5cdb383cef9c -r 72d003e82349 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 20 09:31:34 2009 +0200
+++ b/QuotMain.thy	Tue Oct 20 09:37:22 2009 +0200
@@ -1114,11 +1114,13 @@
 (****************************)
 
 (* some helper functions *)
+
+
 ML {*
-fun mk_babs ty ty' = Const (@{const_name "Babs"}, (ty' --> @{typ bool}) --> ty --> ty)
+fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
-fun mk_resp ty = Const (@{const_name Respects}, ([ty, ty] ---> @{typ bool}) --> ty --> @{typ bool})
+fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
 *}
 
 (* applies f to the subterm of an abstractions, otherwise to the given term *)
@@ -1179,7 +1181,7 @@
   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
 *}
 
-(* my version is not eta-expanded *)
+(* my version is not eta-expanded, but that should be OK *)
 ML {*  
   cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
   cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})