diff -r 7a1636c3ffc9 -r 6aa76ce59ef2 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:37 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:40 2009 +0200
@@ -8,7 +8,7 @@
   type specification_table;
   val make_const_spec_table : theory -> specification_table
   val get_specification :  specification_table -> string -> thm list
-  val obtain_specification_graph : specification_table -> string -> thm list Graph.T
+  val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T
   val normalize_equation : theory -> thm -> thm
 end;
 
@@ -195,8 +195,6 @@
     @{const_name Nat.one_nat_inst.one_nat},
 @{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
 @{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
-@{const_name "Nat.nat.nat_case"}, @{const_name "List.list.list_case"},
-@{const_name "Option.option.option_case"},
 @{const_name Nat.ord_nat_inst.less_eq_nat},
 @{const_name number_nat_inst.number_of_nat},
   @{const_name Int.Bit0},
@@ -205,13 +203,16 @@
 @{const_name "Int.zero_int_inst.zero_int"},
 @{const_name "List.filter"}]
 
-fun obtain_specification_graph table constname =
+fun case_consts thy s = is_some (Datatype.info_of_case thy s)
+
+fun obtain_specification_graph thy table constname =
   let
     fun is_nondefining_constname c = member (op =) logic_operator_names c
     val is_defining_constname = member (op =) (Symtab.keys table)
     fun defiants_of specs =
       fold (Term.add_const_names o prop_of) specs []
       |> filter is_defining_constname
+      |> filter_out (case_consts thy)
       |> filter_out special_cases
     fun extend constname =
       let