adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog

--- a/src/HOL/IsaMakefile	Mon Sep 06 15:01:37 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
@@ -244,6 +244,8 @@
   Map.thy \
   Nat_Numeral.thy \
   Nat_Transfer.thy \
+  New_DSequence.thy \
+  New_Random_Sequence.thy \
   Nitpick.thy \
   Numeral_Simprocs.thy \
   Presburger.thy \

--- a/src/HOL/New_DSequence.thy	Mon Sep 06 15:01:37 2010 +0200
+++ b/src/HOL/New_DSequence.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -83,7 +83,7 @@
 
 definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
 where
-  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
+  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
 
 definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
 where

--- 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)