--- a/QuotMain.thy	Tue Oct 06 02:02:51 2009 +0200
+++ b/QuotMain.thy	Tue Oct 06 09:28:59 2009 +0200
@@ -739,18 +739,14 @@
   val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
   
   val thy = ProofContext.theory_of ctxt'
-  fun get_lhs xs = 
-  let 
-    val cxs = map (cterm_of thy o Free) xs
-  in
-    Drule.list_comb (lhs, cxs)
-  end
+  val cxs = map (cterm_of thy o Free) xs
+  val new_lhs = Drule.list_comb (lhs, cxs)
 
   fun get_conv [] = Conv.rewr_conv def
     | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
  
 in
-  get_conv xs (get_lhs xs) |>  
+  get_conv xs new_lhs |>  
   singleton (ProofContext.export ctxt' ctxt)
 end
 *}
@@ -762,10 +758,14 @@
 term membship
 term IN
 thm IN_def
-ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"}*}
+
+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 {* unlam_def @{context} @{thm IN_def} *}
+ML {* @{thm IN_def}; unlam_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]