changeset 29288 | 253bcf2a5854 |
parent 29272 | fb3ccf499df5 |
child 29432 | 5bb5551bef03 |
--- a/src/Pure/thm.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/Pure/thm.ML Thu Jan 01 14:23:39 2009 +0100 @@ -1695,7 +1695,7 @@ val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ oracles = NameSpace.merge_tables (op =) oracles + fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles handle Symtab.DUP dup => err_dup_ora dup; );