# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1254822095 -7200
# Node ID e8660818c755d08c2da330264b68f39b90c1235f
# Parent  221e926da073fc19bf5ab066f32d08204a984dce
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)

diff -r 221e926da073 -r e8660818c755 QuotMain.thy
--- 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 =