--- a/Nominal/nominal_termination.ML	Tue Jul 19 10:43:43 2011 +0200
+++ b/Nominal/nominal_termination.ML	Tue Jul 19 19:09:06 2011 +0100
@@ -52,7 +52,12 @@
           val tsimps = map remove_domain_condition psimps
           val tinduct = map remove_domain_condition pinducts
           val teqvts = map remove_domain_condition eqvts
-  
+
+          val _ = tracing ("tot psimps1:\n" ^ cat_lines (map @{make_string} psimps))
+          val _ = tracing ("tot psimps2:\n" ^ cat_lines (map @{make_string} tsimps))
+          val _ = tracing ("tot induct1:\n" ^ cat_lines (map @{make_string} pinducts))
+          val _ = tracing ("tot induct2:\n" ^ cat_lines (map @{make_string} tinduct))
+
           fun qualify n = Binding.name n
             |> Binding.qualify true defname
         in
@@ -66,7 +71,7 @@
           |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy =>
             let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
               case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
-              simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=eqvts }
+              simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts }
             in
               (info',
                lthy