| changeset 42375 | 774df7c59508 |
| parent 42361 | 23f352990944 |
| child 44005 | 421f8bc19ce4 |
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Sun Apr 17 13:47:22 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Sun Apr 17 19:54:04 2011 +0200 @@ -44,7 +44,7 @@ fun add_arity ((b, sorts, mx), sort) thy : theory = thy - |> Sign.add_types [(b, length sorts, mx)] + |> Sign.add_types_global [(b, length sorts, mx)] |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort) fun gen_add_domain