# HG changeset patch
# User kuncar
# Date 1379425751 -7200
# Node ID 339aefeacb578f3175a69bbaccbe389410c3e790
# Parent  e6adad558def78bee5da292716f7f7f9a6bb7355
correct merging of restore data

diff -r e6adad558def -r 339aefeacb57 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue Sep 17 15:18:14 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Sep 17 15:49:11 2013 +0200
@@ -57,6 +57,25 @@
   pos_distr_rules: thm list, neg_distr_rules: thm list}
 type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
 
+fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
+           {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 
+           Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
+
+fun option_eq _ (NONE,NONE) = true
+  | option_eq _ (NONE,_) = false
+  | option_eq _ (_,NONE) = false
+  | option_eq cmp (SOME x, SOME y) = cmp (x,y);
+
+fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
+                {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
+                Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
+
+fun join_restore_data key (rd1, rd2) =
+  if pointer_eq (rd1, rd2) then raise Symtab.SAME else
+  if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else
+    { quotient = #quotient rd1, 
+      transfer_rules = Item_Net.merge (#transfer_rules rd1, #transfer_rules rd2)}
+
 structure Data = Generic_Data
 (
   type T = 
@@ -83,7 +102,7 @@
       quotients = Symtab.merge (K true) (q1, q2),
       reflexivity_rules = Item_Net.merge (rr1, rr2),
       relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
-      restore_data = Symtab.merge (K true) (rd1, rd2) }
+      restore_data = Symtab.join join_restore_data (rd1, rd2) }
 )
 
 fun map_data f1 f2 f3 f4 f5
@@ -183,19 +202,6 @@
 
 (* info about quotient types *)
 
-fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
-           {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 
-           Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
-
-fun option_eq _ (NONE,NONE) = true
-  | option_eq _ (NONE,_) = false
-  | option_eq _ (_,NONE) = false
-  | option_eq cmp (SOME x, SOME y) = cmp (x,y);
-
-fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
-                {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
-                Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
-
 fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
   {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}