--- a/QuotMain.thy	Thu Oct 22 01:59:17 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 06:51:27 2009 +0200
@@ -741,8 +741,6 @@
 
     fun mk_abs tm =
       let
-        val _ = tracing (Syntax.string_of_term @{context} tm)
-        val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
         val ty = exchange_ty rty qty (fastype_of tm) in
       fst (get_fun absF rty qty lthy ty) $ tm end
 
@@ -771,7 +769,6 @@
       end
     | x =>
       let
-        val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
         val (opp, tms0) = Term.strip_comb tm
         val tms = map (build_aux lthy) tms0
         val ty = fastype_of tm
@@ -781,7 +778,7 @@
       else if (is_constructor opp andalso needs_lift rty ty) then
           mk_rep (mk_abs (list_comb (opp,tms)))
         else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
-            mk_rep(mk_abs(list_comb(opp,tms)))
+          mk_rep(mk_abs(list_comb(opp,tms)))
         else if tms = [] then opp
         else list_comb(opp, tms)
       end