# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259146019 -3600
# Node ID 5507e972ec727134fd934176fdc688a4763600f3
# Parent  57bde65f6eb23c0bb750339190ff2c1394c465c1
deleted some obsolete diagnostic code

diff -r 57bde65f6eb2 -r 5507e972ec72 QuotMain.thy
--- 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