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;