--- 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