src/Pure/theory.ML
changeset 17496 26535df536ae
parent 17038 6dbd7c63a5a6
child 17706 e534e39f3531
--- a/src/Pure/theory.ML	Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/theory.ML	Tue Sep 20 08:21:49 2005 +0200
@@ -120,7 +120,7 @@
 
       val axioms = NameSpace.empty_table;
       val defs = Defs.merge pp defs1 defs2;
-      val oracles = NameSpace.merge_tables eq_snd (oracles1, oracles2)
+      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
         handle Symtab.DUPS dups => err_dup_oras dups;
     in make_thy (axioms, defs, oracles) end;