--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Feb 23 15:15:59 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Feb 23 15:49:40 2012 +0100
@@ -132,7 +132,7 @@
val _ = print_step options "Fetching definitions from theory..."
val gr = cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
(fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
- |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
+ |> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr))
val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
in
cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"