src/Pure/net.ML
changeset 16842 5979c46853d1
parent 16808 644fc45c7292
child 16938 04bdd18e0ad1
     1.1 --- a/src/Pure/net.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/net.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -222,10 +222,10 @@
     1.4        | subtr (Leaf _) (net as Net _) = subtr emptynet net
     1.5        | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
     1.6              (Net {comb = comb2, var = var2, atoms = atoms2}) =
     1.7 -          Symtab.fold (fn (a, net) =>
     1.8 -            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2 o
     1.9 -          subtr var1 var2 o
    1.10 -          subtr comb1 comb2;
    1.11 +          subtr comb1 comb2
    1.12 +          #> subtr var1 var2
    1.13 +          #> Symtab.fold (fn (a, net) =>
    1.14 +            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2
    1.15    in subtr net1 net2 [] end;
    1.16  
    1.17  fun entries net = subtract (K false) empty net;