diff -r 99cb0d80ff32 -r 967fda58d1b2 src/Tools/isac/ProgLang/rewrite.sml
--- a/src/Tools/isac/ProgLang/rewrite.sml	Fri Oct 01 17:27:55 2010 +0200
+++ b/src/Tools/isac/ProgLang/rewrite.sml	Fri Oct 01 18:25:06 2010 +0200
@@ -190,10 +190,6 @@
 		    (let val subst: Type.tyenv * Envir.tenv = 
 			     Pattern.match thy (pat, t)
 					    (Vartab.empty, Vartab.empty)
-			 val _ = tracing ("app_rev: pres=------------------");
-			 val _ = tracing ("app_rev: pres=" ^ terms2str pres);
-			 val _ = tracing ("app_rev: pat =" ^ term2str pat);
-			 val _ = tracing ("app_rev: t   =" ^ term2str t);
 		     in snd (eval__true thy (i+1) 
 					(map (Envir.subst_term subst) pres)
 					[] erls)