src/Pure/net.ML
changeset 55741 b969263fcf02
parent 45404 69ec395ef6ca
child 56137 af71fb1cb31f
     1.1 --- a/src/Pure/net.ML	Tue Feb 25 11:36:04 2014 +0100
     1.2 +++ b/src/Pure/net.ML	Tue Feb 25 12:53:08 2014 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4    val encode_type: typ -> term
     1.5    type 'a net
     1.6    val empty: 'a net
     1.7 +  val is_empty: 'a net -> bool
     1.8    exception INSERT
     1.9    val insert: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net
    1.10    val insert_term: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net
    1.11 @@ -251,7 +252,8 @@
    1.12        map (cons_fst VarK) (dest var) @
    1.13        maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
    1.14  
    1.15 -fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
    1.16 +fun merge eq (net1, net2) =
    1.17 +  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-standard merge order!?! *)
    1.18  
    1.19  fun content net = map #2 (dest net);
    1.20