# HG changeset patch
# User bulwahn
# Date 1304675841 -7200
# Node ID 42d607a9ae6557941712b047b94c2ec21fbd40be
# Parent  936cd1c493b49ea7ce5b8b0997e6dcb92f49999f
improving merge of code specifications by removing code equations of constructors after merging two theories

diff -r 936cd1c493b4 -r 42d607a9ae65 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu May 05 23:54:06 2011 +0200
+++ b/src/Pure/Isar/code.ML	Fri May 06 11:57:21 2011 +0200
@@ -201,6 +201,7 @@
   let
     val signatures = (Symtab.merge (op =) (tycos1, tycos2),
       Symtab.merge typ_equiv (sigs1, sigs2));
+    val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2);
     fun merge_functions ((_, history1), (_, history2)) =
       let
         val raw_history = AList.merge (op = : serial * serial -> bool)
@@ -209,8 +210,10 @@
         val history = if null filtered_history
           then raw_history else filtered_history;
       in ((false, (snd o hd) history), history) end;
-    val functions = Symtab.join (K merge_functions) (functions1, functions2);
-    val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2);
+    val all_constructors =
+      maps (map fst o fst o constructors_of o snd o snd o hd o snd) (Symtab.dest types);
+    val functions = Symtab.join (K merge_functions) (functions1, functions2)
+      |> fold (fn c => Symtab.map_entry c (apfst (K (true, empty_fun_spec)))) all_constructors;
     val cases = (Symtab.merge (K true) (cases1, cases2),
       Symtab.merge (K true) (undefs1, undefs2));
   in make_spec (false, ((signatures, functions), (types, cases))) end;