diff -r d1038e67923a -r b95a2065aa10 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_function.ML	Tue Jul 19 01:40:36 2011 +0100
@@ -156,9 +156,6 @@
           termination, domintros, cases, eqvts, ...} =
           cont (Thm.close_derivation proof)
   
-        val _ = tracing ("final psimps:\n" ^ cat_lines (map @{make_string} psimps))
-        val _ = tracing ("final eqvts:\n" ^ cat_lines (map @{make_string} eqvts))
-
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
           |> Binding.qualify true defname
@@ -184,8 +181,6 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
 
-        val _ = tracing ("final final psimps:\n" ^ cat_lines (map @{make_string} psimps'))
-
         val _ =
           if not is_external then ()
           else Specification.print_consts lthy (K false) (map fst fixes)