# HG changeset patch
# User haftmann
# Date 1242282127 -7200
# Node ID bdc1504ad456d4e7e81867625c4479229a1d4ff9
# Parent  2ce5c0c4d69728bfe64712ff34c7bd15c213f2d7
dropped accidental debug messages

diff -r 2ce5c0c4d697 -r bdc1504ad456 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Thu May 14 08:22:06 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Thu May 14 08:22:07 2009 +0200
@@ -72,9 +72,7 @@
         map Free (Name.names Name.context "a" tys));
       val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
         (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
-        handle TYPE (msg, tys, ts) => (tracing msg; error "")
       val cty = Thm.ctyp_of thy ty;
-      val _ = tracing (cat_lines [makestring arg, makestring rhs, makestring cty])
     in
       @{thm term_of_anything}
       |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]