| changeset 4627 | ae95666c71cc |
| parent 4617 | cea2a5b5ee10 |
| child 4786 | 9b6072bd71e4 |
--- a/src/Pure/theory.ML Thu Feb 12 16:54:01 1998 +0100 +++ b/src/Pure/theory.ML Thu Feb 12 17:43:53 1998 +0100 @@ -385,7 +385,7 @@ (** merge theories **) (*exception ERROR*) fun merge_sign (sg, thy) = - Sign.merge (sg, sign_of thy) handle TERM (msg, _) => error msg; + Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg; (*merge list of theories from left to right, preparing extend*) fun prep_ext_merge thys =