1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -281,9 +281,10 @@
     1.4            | itr (a::rst) = i=a orelse itr rst
     1.5      in itr L end;
     1.6  
     1.7 +infix union;
     1.8  fun [] union S = S
     1.9    | S union [] = S
    1.10 -  | (a::rst) union S2 = rst union (insert (op =) a S2)
    1.11 +  | (a::rst) union S2 = rst union (insert (op =) a S2);
    1.12  
    1.13  fun implode_subst [] = []
    1.14    | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
    1.15 @@ -1229,7 +1230,7 @@
    1.16            | add_consts (_, cs) = cs
    1.17          val t_consts = add_consts(t,[])
    1.18      in
    1.19 -        fn th => eq_set(t_consts,add_consts(prop_of th,[]))
    1.20 +        fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, []))
    1.21      end
    1.22  
    1.23  fun split_name str =