# HG changeset patch
# User bulwahn
# Date 1256630636 -3600
# Node ID 8bd2eb003b8f87cd61b7bdf32c47439574add628
# Parent  4b13ab778b7824ee8c381b70aa343fe609b46a7a
print retrieved specification when printing intermediate results

diff -r 4b13ab778b78 -r 8bd2eb003b8f src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -99,7 +99,7 @@
   let
     val _ = print_step options "Fetching definitions from theory..."
     val table = Predicate_Compile_Data.make_const_spec_table thy
-    val gr = Predicate_Compile_Data.obtain_specification_graph thy table const
+    val gr = Predicate_Compile_Data.obtain_specification_graph options thy table const
     val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
   in fold_rev (preprocess_strong_conn_constnames options gr)
     (Graph.strong_conn gr) thy
diff -r 4b13ab778b78 -r 8bd2eb003b8f src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -8,7 +8,8 @@
   type specification_table;
   val make_const_spec_table : theory -> specification_table
   val get_specification :  specification_table -> string -> thm list
-  val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T
+  val obtain_specification_graph : Predicate_Compile_Aux.options -> theory ->
+    specification_table -> string -> thm list Graph.T
   val normalize_equation : theory -> thm -> thm
 end;
 
@@ -186,7 +187,13 @@
 
 fun case_consts thy s = is_some (Datatype.info_of_case thy s)
 
-fun obtain_specification_graph thy table constname =
+fun print_specification options thy constname specs = 
+  if show_intermediate_results options then
+    tracing ("Specification of " ^ constname ^ ":\n" ^
+      cat_lines (map (Display.string_of_thm_global thy) specs))
+  else ()
+
+fun obtain_specification_graph options thy table constname =
   let
     fun is_nondefining_constname c = member (op =) logic_operator_names c
     val is_defining_constname = member (op =) (Symtab.keys table)
@@ -201,6 +208,7 @@
     fun extend constname =
       let
         val specs = get_specification table constname
+        val _ = print_specification options thy constname specs
       in (specs, defiants_of specs) end;
   in
     Graph.extend extend constname Graph.empty