merge: drops path elements;
authorwenzelm
Mon Oct 13 12:48:23 1997 +0200 (1997-10-13)
changeset 3850305e5adfd7c8
parent 3849 3ea10bfd329d
child 3851 fe9932a7cd46
merge: drops path elements;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Oct 13 11:00:06 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Oct 13 12:48:23 1997 +0200
     1.3 @@ -789,7 +789,7 @@
     1.4      (*neither is union already; must form union*)
     1.5      let
     1.6        val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
     1.7 -        path, spaces = spaces1, stamps = stamps1} = sg1;
     1.8 +        path = _, spaces = spaces1, stamps = stamps1} = sg1;
     1.9        val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
    1.10          path = _, spaces = spaces2, stamps = stamps2} = sg2;
    1.11  
    1.12 @@ -816,7 +816,7 @@
    1.13              (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
    1.14      in
    1.15        Sg {tsig = tsig, const_tab = const_tab, syn = syn,
    1.16 -        path = path, spaces = spaces, stamps = stamps}
    1.17 +        path = [], spaces = spaces, stamps = stamps}
    1.18      end;
    1.19  
    1.20  fun merge sgs =