diff -r e003e5e36bae -r cd5614027c53 Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Wed Jan 19 17:11:10 2011 +0100
+++ b/Nominal/nominal_inductive.ML	Wed Jan 19 17:54:06 2011 +0100
@@ -24,13 +24,13 @@
 
 fun mk_cminus p = Thm.capply @{cterm "uminus :: perm => perm"} p 
 
-
 fun minus_permute_intro_tac p = 
   rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})
 
 fun minus_permute_elim p thm = 
   thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
 
+(* fixme: move to nominal_library *)
 fun real_head_of (@{term Trueprop} $ t) = real_head_of t
   | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t
   | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t
@@ -56,6 +56,7 @@
     if null avoid then [] else [vc_goal, finite_goal]
   end
 
+(* fixme: move to nominal_library *)
 fun map_term prop f trm =
   if prop trm 
   then f trm
@@ -120,11 +121,13 @@
     mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl'
   end
 
+(* fixme: move to nominal_library *)
 fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2)
   | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2)
   | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2)
   | same_name _ = false
 
+(* fixme: move to nominal_library *)
 fun map7 _ [] [] [] [] [] [] [] = []
   | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = 
       f x y z u v r s :: map7 f xs ys zs us vs rs ss
@@ -150,12 +153,8 @@
       val prm' = (prems' MRS prm)
         |> flag ? (all_elims [p])
         |> flag ? (eqvt_srule context)
-
-      val _ = tracing ("prm':" ^ @{make_string} prm')
     in
-      print_tac "start helper"
-      THEN asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1
-      THEN print_tac "final helper"
+      asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1
     end) ctxt
 
 fun non_binder_tac prem intr_cvars Ps ctxt = 
@@ -252,20 +251,12 @@
       fun select prm (t, i) =
         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
 
-      val _ = tracing ("fthm:\n" ^ @{make_string} fthm)
-      val _ = tracing ("fr_eqs:\n" ^ cat_lines (map @{make_string} fresh_eqs))
-      val _ = tracing ("fprop:\n" ^ @{make_string} fprop)
-      val _ = tracing ("fprop':\n" ^ @{make_string} fprop')
-      val _ = tracing ("fperm:\n" ^ @{make_string} q)
-      val _ = tracing ("prem':\n" ^ @{make_string} prem')
-
       val side_thm = Goal.prove ctxt' [] [] (term_of concl)
         (fn {context, ...} => 
            EVERY1 [ CONVERSION (expand_conv_bot context),
                     eqvt_stac context,
                     rtac prem',
-                    RANGE (tac_fresh :: map (SUBGOAL o select) prems),
-                    K (print_tac "GOAL") ])
+                    RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
         |> singleton (ProofContext.export ctxt' ctxt)        
     in
       rtac side_thm 1
@@ -364,9 +355,6 @@
         val attrs = 
           [ Attrib.internal (K (Rule_Cases.consumes 1)),
             Attrib.internal (K (Rule_Cases.case_names rule_names)) ]
-        val _ = tracing ("RESULTS\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) strong_ind_thms))
-        val _ = tracing ("rule_names: " ^ commas rule_names)
-        val _ = tracing ("pred_names: " ^ commas pred_names)
       in
         ctxt
         |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms)