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