--- a/QuotMain.thy	Tue Oct 06 11:36:08 2009 +0200
+++ b/QuotMain.thy	Tue Oct 06 11:41:35 2009 +0200
@@ -719,7 +719,7 @@
   done
 
 text {*
-  Unlam_def converts a definition given as
+  Unabs_def converts a definition given as
 
     c \<equiv> %x. %y. f x y
 
@@ -732,7 +732,7 @@
 *}
 
 ML {*
-fun unlam_def ctxt def =
+fun unabs_def ctxt def =
 let
   val (lhs, rhs) = Thm.dest_equals (cprop_of def)
   val xs = strip_abs_vars (term_of rhs)
@@ -758,10 +758,10 @@
 term IN
 thm IN_def
 
-(* unlam_def tests *)
+(* unabs_def tests *)
 ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *}
 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*}
-ML {* @{thm IN_def}; unlam_def @{context} @{thm IN_def} *}
+ML {* @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
 
 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
@@ -932,7 +932,7 @@
 
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
-ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}
+ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
 ML {*
   fun dest_cbinop t =