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