# HG changeset patch
# User bulwahn
# Date 1249368303 -7200
# Node ID 39a6a0800c6c4810c09193fb437d40e1a51f80e0
# Parent  bca7fd8498297d3684f15591b2c1dfe463150799
removing tracing messages in predicate compiler

diff -r bca7fd849829 -r 39a6a0800c6c src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:45:03 2009 +0200
@@ -1154,9 +1154,7 @@
   case strip_comb t of
     (Const (name, T), params) =>
        let
-         val _ = Output.tracing (Syntax.string_of_term_global thy t)
          val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params)
-         val _ = Output.tracing "..."
          val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
        in
          list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params')
@@ -1870,9 +1868,6 @@
     val nparams = nparams_of thy (hd prednames)
     val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
     val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs)
-    (*val _ = Output.tracing ("extra_modes are: " ^
-      cat_lines (map (fn (name, modes) => name ^ " has modes:" ^
-      (commas (map string_of_mode modes))) extra_modes)) *)
     val _ $ u = Logic.strip_imp_concl (hd intrs);
     val params = List.take (snd (strip_comb u), nparams);
     val param_vs = maps term_vs params