# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1296701824 0
# Node ID e8c1a19e13d22a8033fea2e07ea6168fc5653953
# Parent  cd336163f270679a92aeda34d483d8e3083ff51b# Parent  08bc1aa259d9e5b20457e93631dd29fa13359ee7
merged

diff -r 08bc1aa259d9 -r e8c1a19e13d2 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue Feb 01 09:07:55 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Thu Feb 03 02:57:04 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