# HG changeset patch
# User wenzelm
# Date 1147367714 -7200
# Node ID d6b806032cccb534dc15198663e80a5045eb7c7b
# Parent  9bf274ec94cf95acbae17dc52c5cb84ce51caafb
tuned Defs.merge;

diff -r 9bf274ec94cf -r d6b806032ccc src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu May 11 19:15:13 2006 +0200
+++ b/src/Pure/theory.ML	Thu May 11 19:15:14 2006 +0200
@@ -120,7 +120,7 @@
       val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
 
       val axioms = NameSpace.empty_table;
-      val defs = Defs.merge pp (defs1, defs2);
+      val defs = Defs.merge (defs1, defs2);
       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;