--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200
@@ -123,9 +123,6 @@
else
error ("unexpected specification for constant " ^ quote constname ^ ":\n"
^ commas (map (quote o Display.string_of_thm_global thy) specs))
- val _ = tracing ("Introduction rules of definitions before flattening: "
- ^ commas (map (Display.string_of_thm ctxt) intros))
- val _ = tracing "Defining local predicates and their intro rules..."
val (intros', (local_defs, thy')) = flatten_intros constname intros thy
val (intross, thy'') = fold_map preprocess local_defs thy'
in