changeset 30447 | 955190fa639b |
parent 30346 | 90efbb8a8cb2 |
child 31723 | f5cafe803b55 |
--- a/src/HOL/Import/proof_kernel.ML Wed Mar 11 15:56:49 2009 +0100 +++ b/src/HOL/Import/proof_kernel.ML Wed Mar 11 15:56:49 2009 +0100 @@ -264,7 +264,6 @@ structure Lib = struct -fun wrap b e s = String.concat[b,s,e] fun assoc x = let @@ -280,9 +279,6 @@ | itr (a::rst) = i=a orelse itr rst in itr L end; -fun mk_set [] = [] - | mk_set (a::rst) = insert (op =) a (mk_set rst) - fun [] union S = S | S union [] = S | (a::rst) union S2 = rst union (insert (op =) a S2)