# HG changeset patch
# User wenzelm
# Date 1392655769 -3600
# Node ID f0ef75c6c0d88b69fa49cad578ada46a1007dbaf
# Parent  6ec3c2c38650f888a42e24f2d93eeb799f6c08cf
more informative error;

diff -r 6ec3c2c38650 -r f0ef75c6c0d8 src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Mon Feb 17 14:59:09 2014 +0100
+++ b/src/HOL/Predicate_Compile.thy	Mon Feb 17 17:49:29 2014 +0100
@@ -81,6 +81,7 @@
   Core_Data.PredData.map (Graph.new_node 
     (@{const_name contains}, 
      Core_Data.PredData {
+       pos = Position.thread_data (),
        intros = [(NONE, @{thm containsI})], 
        elim = SOME @{thm containsE}, 
        preprocessed = true,
diff -r 6ec3c2c38650 -r f0ef75c6c0d8 src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Feb 17 14:59:09 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Feb 17 17:49:29 2014 +0100
@@ -18,6 +18,7 @@
   };
 
   datatype pred_data = PredData of {
+    pos : Position.T,
     intros : (string option * thm) list,
     elim : thm option,
     preprocessed : bool,
@@ -100,6 +101,7 @@
   PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
 
 datatype pred_data = PredData of {
+  pos: Position.T,
   intros : (string option * thm) list,
   elim : thm option,
   preprocessed : bool,
@@ -109,13 +111,17 @@
 };
 
 fun rep_pred_data (PredData data) = data;
+val pos_of = #pos o rep_pred_data;
 
-fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
-  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
+fun mk_pred_data
+    (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) =
+  PredData {pos = pos, intros = intros, elim = elim, preprocessed = preprocessed,
     function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
 
-fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
-  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
+fun map_pred_data f
+    (PredData {pos, intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
+  mk_pred_data
+    (f (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))))
 
 fun eq_option eq (NONE, NONE) = true
   | eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -130,7 +136,13 @@
   type T = pred_data Graph.T;
   val empty = Graph.empty;
   val extend = I;
-  val merge = Graph.merge eq_pred_data;
+  val merge =
+    Graph.join (fn key => fn (x, y) =>
+      if eq_pred_data (x, y)
+      then raise Graph.SAME
+      else
+        error ("Duplicate predicate declarations for " ^ quote key ^
+          Position.here (pos_of x) ^ Position.here (pos_of y)));
 );
 
 
@@ -260,11 +272,13 @@
   (case try (Inductive.the_inductive ctxt) name of
     SOME (info as (_, result)) => 
       let
+        val thy = Proof_Context.theory_of ctxt
+
+        val pos = Position.thread_data ()
         fun is_intro_of intro =
           let
             val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
           in (fst (dest_Const const) = name) end;
-        val thy = Proof_Context.theory_of ctxt
         val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
         val index = find_index (fn s => s = name) (#names (fst info))
         val pre_elim = nth (#elims result) index
@@ -273,13 +287,13 @@
         val nparams = length (Inductive.params_of (#raw_induct result))
         val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
       in
-        mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
+        mk_pred_data (pos, (((map (pair NONE) intros, SOME elim), true), no_compilation))
       end
   | NONE => error ("No such predicate: " ^ quote name))
 
 fun add_predfun_data name mode data =
   let
-    val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
+    val add = (apsnd o apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
 fun is_inductive_predicate ctxt name =
@@ -305,17 +319,21 @@
       (case try (Graph.get_node gr) name of
         SOME _ =>
           Graph.map_node name (map_pred_data
-            (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
+            (apsnd (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))))) gr
       | NONE =>
           Graph.new_node
-            (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr)
+            (name,
+              mk_pred_data (Position.thread_data (),
+                (((([(opt_case_name, thm)], NONE), false), no_compilation)))) gr)
   in PredData.map cons_intro thy end
 
 fun set_elim thm =
   let
     val (name, _) =
       dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
-  in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
+  in
+    PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
+  end
 
 fun register_predicate (constname, intros, elim) thy =
   let
@@ -324,7 +342,8 @@
     if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
       PredData.map
         (Graph.new_node (constname,
-          mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
+          mk_pred_data (Position.thread_data (),
+            (((named_intros, SOME elim), false), no_compilation)))) thy
     else thy
   end
 
@@ -345,14 +364,14 @@
 
 fun defined_function_of compilation pred =
   let
-    val set = (apsnd o apfst) (cons (compilation, []))
+    val set = (apsnd o apsnd o apfst) (cons (compilation, []))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
 
 fun set_function_name compilation pred mode name =
   let
-    val set = (apsnd o apfst)
+    val set = (apsnd o apsnd o apfst)
       (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
@@ -360,7 +379,7 @@
 
 fun set_needs_random name modes =
   let
-    val set = (apsnd o apsnd o apsnd) (K modes)
+    val set = (apsnd o apsnd o apsnd o apsnd) (K modes)
   in
     PredData.map (Graph.map_node name (map_pred_data set))
   end  
@@ -389,7 +408,7 @@
   end
 
 fun preprocess_intros name thy =
-  PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
+  PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (fn (rules, preprocessed) =>
     if preprocessed then (rules, preprocessed)
     else
       let
@@ -401,7 +420,7 @@
         val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
       in
         ((named_intros', SOME elim'), true)
-      end))))
+      end)))))
     thy  
 
 
@@ -422,7 +441,7 @@
   AList.lookup eq_mode
     (Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode
 
-fun force_modes_and_compilations pred_name compilations =
+fun force_modes_and_compilations pred_name compilations thy =
   let
     (* thm refl is a dummy thm *)
     val modes = map fst compilations
@@ -435,11 +454,14 @@
       map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
     val alt_compilations = map (apsnd fst) compilations
   in
+    thy |>
     PredData.map
       (Graph.new_node
         (pred_name,
-          mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
-    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
+          mk_pred_data
+            (Position.thread_data (),
+              ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random))))))
+    |> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   end
 
 fun functional_compilation fun_name mode compfuns T =