src/Pure/theory.ML
changeset 19614 d6b806032ccc
parent 19592 856cd7460168
child 19630 d370c3f5d3b2
     1.1 --- a/src/Pure/theory.ML	Thu May 11 19:15:13 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu May 11 19:15:14 2006 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4        val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
     1.5  
     1.6        val axioms = NameSpace.empty_table;
     1.7 -      val defs = Defs.merge pp (defs1, defs2);
     1.8 +      val defs = Defs.merge (defs1, defs2);
     1.9        val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
    1.10          handle Symtab.DUPS dups => err_dup_oras dups;
    1.11      in make_thy (axioms, defs, oracles) end;