# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1296701517 0
# Node ID cd336163f270679a92aeda34d483d8e3083ff51b
# Parent  7eebe0d5d298d101bb2fcd61f16c7cd14a96de1e
removed diagnostic code

diff -r 7eebe0d5d298 -r cd336163f270 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Sat Jan 29 14:26:47 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Thu Feb 03 02:51:57 2011 +0000
@@ -483,9 +483,6 @@
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
  
-    val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm)
-    val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt)
-
     val _ = trace_msg (K "Proving Replacement lemmas...")
     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses