clean up debugging output
authorblanchet
Tue Oct 05 11:14:56 2010 +0200 (2010-10-05)
changeset 399527fb79905ed72
parent 39951 ff60a6e4edfe
child 39953 aa54f347e5e2
clean up debugging output
src/HOL/Tools/Metis/metis_tactics.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 11:10:37 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 11:14:56 2010 +0200
     1.3 @@ -64,10 +64,10 @@
     1.4        [] |> Vartab.fold (fn (z, (S, T)) =>
     1.5                              cons (TVar (z, S), Type.devar tyenv T)) tyenv
     1.6      val inst = inst |> map (pairself (subst_atomic_types instT))
     1.7 -    val _ = tracing (cat_lines (map (fn (T, U) =>
     1.8 +    val _ = trace_msg (fn () => cat_lines (map (fn (T, U) =>
     1.9          Syntax.string_of_typ @{context} T ^ " |-> " ^
    1.10          Syntax.string_of_typ @{context} U) instT))
    1.11 -    val _ = tracing (cat_lines (map (fn (t, u) =>
    1.12 +    val _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
    1.13          Syntax.string_of_term @{context} t ^ " |-> " ^
    1.14          Syntax.string_of_term @{context} u) inst))
    1.15      val cinstT = instT |> map (pairself (ctyp_of thy))
    1.16 @@ -292,15 +292,11 @@
    1.17        Goal.prove ctxt [] [] @{prop False}
    1.18            (K (cut_rules_tac
    1.19                    (map (fst o the o nth axioms o fst o fst) ax_counts) 1
    1.20 -              THEN print_tac "cut:"
    1.21                THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
    1.22                THEN copy_prems_tac (map snd ax_counts) [] 1
    1.23 -              THEN print_tac "eliminated exist and copied prems:"
    1.24                THEN release_clusters_tac thy ax_counts substs params0
    1.25                                          ordered_clusters 1
    1.26 -              THEN print_tac "released clusters:"
    1.27                THEN match_tac [prems_imp_false] 1
    1.28 -              THEN print_tac "applied rule:"
    1.29                THEN ALLGOALS (fn i =>
    1.30                         rtac @{thm skolem_COMBK_I} i
    1.31                         THEN rotate_tac (rotation_for_subgoal i) i