author | haftmann |
Wed, 11 Mar 2009 15:56:49 +0100 | |
changeset 30447 | 955190fa639b |
parent 30446 | e3641cac56fa |
child 30448 | 0c7e1578036c |
--- 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)