--- a/QuotMain.thy	Wed Nov 25 11:58:56 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 11:59:49 2009 +0100
@@ -737,13 +737,7 @@
        then rtrm
        else rtrm (* FIXME: check correspondence according to definitions *) 
   | (rt, qt) => 
-     let
-       val _ = tracing "default execption"
-       val _ = tracing (PolyML.makestring rt)
-       val _ = tracing (PolyML.makestring qt)
-     in
        raise (LIFT_MATCH "regularize (default)")
-     end
 *}
 
 ML {*
@@ -885,7 +879,6 @@
 (* bound variables need to be treated properly,  *)
 (* as the type of subterms need to be calculated *)
 
-
 fun inj_REPABS lthy (rtrm, qtrm) =
 let
   val rty = fastype_of rtrm