# HG changeset patch
# User wenzelm
# Date 876739703 -7200
# Node ID 305e5adfd7c88396451c712d4ca55ca3097221e8
# Parent  3ea10bfd329d26c5501b7c4d93e84439e9f3bbd0
merge: drops path elements;

diff -r 3ea10bfd329d -r 305e5adfd7c8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Oct 13 11:00:06 1997 +0200
+++ b/src/Pure/sign.ML	Mon Oct 13 12:48:23 1997 +0200
@@ -789,7 +789,7 @@
     (*neither is union already; must form union*)
     let
       val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
-        path, spaces = spaces1, stamps = stamps1} = sg1;
+        path = _, spaces = spaces1, stamps = stamps1} = sg1;
       val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
         path = _, spaces = spaces2, stamps = stamps2} = sg2;
 
@@ -816,7 +816,7 @@
             (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
     in
       Sg {tsig = tsig, const_tab = const_tab, syn = syn,
-        path = path, spaces = spaces, stamps = stamps}
+        path = [], spaces = spaces, stamps = stamps}
     end;
 
 fun merge sgs =