--- a/src/HOL/Import/proof_kernel.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Oct 20 16:13:01 2009 +0200
@@ -281,9 +281,10 @@
| itr (a::rst) = i=a orelse itr rst
in itr L end;
+infix union;
fun [] union S = S
| S union [] = S
- | (a::rst) union S2 = rst union (insert (op =) a S2)
+ | (a::rst) union S2 = rst union (insert (op =) a S2);
fun implode_subst [] = []
| implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
@@ -1229,7 +1230,7 @@
| add_consts (_, cs) = cs
val t_consts = add_consts(t,[])
in
- fn th => eq_set(t_consts,add_consts(prop_of th,[]))
+ fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, []))
end
fun split_name str =