--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:37 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:40 2009 +0200
@@ -56,7 +56,7 @@
let
val _ = Output.tracing ("Fetching definitions from theory...")
val table = Pred_Compile_Data.make_const_spec_table thy
- val gr = Pred_Compile_Data.obtain_specification_graph table const
+ val gr = Pred_Compile_Data.obtain_specification_graph thy table const
val _ = Output.tracing (commas (Graph.all_succs gr [const]))
val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
in fold_rev (preprocess_strong_conn_constnames gr)