--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 20 22:46:19 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 20 23:35:30 2011 +0200
@@ -303,7 +303,7 @@
val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
Termtab.update (const, consts)) consts) constss;
fun succs consts = consts
- |> maps (Term_Graph.imm_succs gr)
+ |> maps (Term_Graph.immediate_succs gr)
|> subtract eq_cname consts
|> map (the o Termtab.lookup mapping)
|> distinct (eq_list eq_cname);