# HG changeset patch
# User bulwahn
# Date 1285582980 -7200
# Node ID ada0cd4900c107bd3f2ce1fda716c876b8ea1eac
# Parent  12cc713036d6c370c2093d1c95ea1f0cf83997da
adding further tracing messages; tuned

diff -r 12cc713036d6 -r ada0cd4900c1 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Sep 27 12:22:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Sep 27 12:23:00 2010 +0200
@@ -315,8 +315,9 @@
         val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
         val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
       in clause end
-    val res = (map translate_intro intros', constant_table')
-  in res end
+  in
+    (map translate_intro intros', constant_table')
+  end
 
 fun depending_preds_of (key, intros) =
   fold Term.add_const_names (map Thm.prop_of intros) []
@@ -669,7 +670,9 @@
   |> (if #ensure_groundness options then
         add_ground_predicates ctxt (#limited_types options)
       else I)
+  |> tap (fn _ => tracing "Adding limited predicates...")
   |> add_limited_predicates (#limited_predicates options)
+  |> tap (fn _ => tracing "Replacing predicates...")
   |> apfst (fold replace (#replacing options))
   |> apfst (reorder_manually (#manual_reorder options))
   |> apfst rename_vars_program