--- a/QuotMain.thy	Wed Nov 25 11:41:42 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 11:46:59 2009 +0100
@@ -856,13 +856,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 {*
@@ -971,7 +965,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