--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 06 15:01:37 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Sep 07 11:51:53 2010 +0200
@@ -309,6 +309,11 @@
fst (extend' key (G, []))
end
+fun print_intros ctxt gr consts =
+ tracing (cat_lines (map (fn const =>
+ "Constant " ^ const ^ "has intros:\n" ^
+ cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
+
fun generate ensure_groundness ctxt const =
let
fun strong_conn_of gr keys =
@@ -316,6 +321,7 @@
val gr = Predicate_Compile_Core.intros_graph_of ctxt
val gr' = add_edges depending_preds_of const gr
val scc = strong_conn_of gr' [const]
+ val _ = print_intros ctxt gr (flat scc)
val constant_table = declare_consts (flat scc) []
in
apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)