src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML

   else ()
 
 fun obtain_specification_graph options thy t =
   let
     fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
-    fun has_code_pred_intros (c, T) = is_some (try (Predicate_Compile_Core.intros_of thy) c)
+    fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of thy) c
     fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
     fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
     fun defiants_of specs =
       fold (Term.add_consts o prop_of) specs []
       |> filter_out is_datatype_constructor

       |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c)
       |> map (fn (c, _) => (c, Sign.the_const_constraint thy c))
       |> map Const
       (*
       |> filter is_defining_constname*)
-    fun extend t =
-      let
-        val specs = get_specification options thy t
-          (*|> Predicate_Compile_Set.unfold_set_notation*)
-        (*val _ = print_specification options thy constname specs*)
-      in (specs, defiants_of specs) end;
+    fun extend t gr =
+      if can (Term_Graph.get_node gr) t then gr
+      else
+        let
+          val specs = get_specification options thy t
+            (*|> Predicate_Compile_Set.unfold_set_notation*)
+          (*val _ = print_specification options thy constname specs*)
+          val us = defiants_of specs
+        in
+          gr
+          |> Term_Graph.new_node (t, specs)
+          |> fold extend us
+          |> fold (fn u => Term_Graph.add_edge (t, u)) us
+        end
   in
-    Term_Graph.extend extend t Term_Graph.empty
+    extend t Term_Graph.empty
   end;
 
 
 fun present_graph gr =
   let