diff -r c8acaded1777 -r 4a00077c008f Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/nominal_termination.ML	Fri Jul 22 11:37:16 2011 +0100
@@ -42,6 +42,7 @@
       val { termination, fs, R, add_simps, case_names, psimps,
         pinducts, defname, eqvts, ...} = info
       val domT = domain_type (fastype_of R)
+
       val goal = HOLogic.mk_Trueprop
                    (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
       fun afterqed [[totality]] lthy =
@@ -50,14 +51,9 @@
           val remove_domain_condition =
             full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
           val tsimps = map remove_domain_condition psimps
-          val tinduct = map remove_domain_condition pinducts
+          val tinducts = 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
@@ -67,7 +63,7 @@
           ||>> Local_Theory.note
              ((qualify "induct",
                [Attrib.internal (K (Rule_Cases.case_names case_names))]),
-              tinduct)
+              tinducts)
           |-> (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,