--- a/Nominal/Fv.thy	Wed Mar 17 17:10:19 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 17:11:23 2010 +0100
@@ -389,16 +389,12 @@
                 val rhs_binds = fv_binds args2 rbinds;
                 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;
                 val rhs = mk_pair (rhs_binds, rhs_arg);
-                val _ = tracing (PolyML.makestring bound_in_ty_nos);
                 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos);
-                val _ = tracing (PolyML.makestring fvs);
                 val fv = mk_compound_fv fvs;
                 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
-                val _ = tracing (PolyML.makestring alphas);
                 val alpha = mk_compound_alpha alphas;
                 val pi = foldr1 add_perm (distinct (op =) rpis);
                 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
-                val _ = tracing (PolyML.makestring alpha_gen_pre);
                 val alpha_gen = Syntax.check_term lthy alpha_gen_pre
               in
                 alpha_gen
@@ -449,7 +445,6 @@
   val fv_names_all = fv_names_fst @ fv_bn_names;
   val add_binds = map (fn x => (Attrib.empty_binding, x))
 (* Function_Fun.add_fun Function_Common.default_config ... true *)
-(*  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*)
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
   val (fvs2, lthy'') =
@@ -596,7 +591,7 @@
   split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
-       add_0_left supp_zero_perm Int_empty_left})
+       add_0_left supp_zero_perm Int_empty_left split_conv})
 *}