# HG changeset patch
# User haftmann
# Date 1447580745 -3600
# Node ID 072012fb4a101b35ba40ae7bec5158741f45b977
# Parent  fd4ac1530d63ecab1f07abb13a95604b3c551265
droppen diagnostic junk from 4b53042d7a40

diff -r fd4ac1530d63 -r 072012fb4a10 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Sat Nov 14 17:37:44 2015 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Sun Nov 15 10:45:45 2015 +0100
@@ -77,13 +77,9 @@
           map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
             (HOLogic.reflect_term t));
     val cty = Thm.global_ctyp_of thy ty;
-    val _ = writeln ("typ: " ^ Syntax.string_of_typ_global thy (Thm.typ_of cty));
-    val _ = writeln ("arg: " ^ Syntax.string_of_term_global thy (Thm.term_of arg));
-    val _ = writeln ("rhs: " ^ Syntax.string_of_term_global thy (Thm.term_of rhs));
   in
     @{thm term_of_anything}
     |> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
-    |> tap (fn _ => writeln "instantiated")
     |> Thm.varifyT_global
   end;