# HG changeset patch
# User bulwahn
# Date 1256396140 -7200
# Node ID 6aa76ce59ef281186acbe69864d8d157c19741ab
# Parent  7a1636c3ffc9cf5efd1c33a8baecc88a581cc21f
added filtering of case constants in the definition retrieval of the predicate compiler

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
diff -r 7a1636c3ffc9 -r 6aa76ce59ef2 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- 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)