# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259146789 -3600
# Node ID 7ccbf4e2eb18415a684ebebafbea3a8100bbc79a
# Parent  991db758a72d269ae0a8666cf04058d049b36d93# Parent  5507e972ec727134fd934176fdc688a4763600f3
Merge

diff -r 991db758a72d -r 7ccbf4e2eb18 QuotMain.thy
--- 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