changeset 25495 | 98f3596bec44 |
parent 25458 | ba8f5e4fa336 |
child 25513 | b7de6e23e143 |
--- a/src/HOL/Tools/typedef_package.ML Wed Nov 28 16:44:18 2007 +0100 +++ b/src/HOL/Tools/typedef_package.ML Wed Nov 28 16:44:20 2007 +0100 @@ -135,7 +135,7 @@ else (NONE, thy); fun typedef_result nonempty = - Typedecl.add (t, vs, mx) + ObjectLogic.typedecl (t, vs, mx) #> snd #> Sign.add_consts_i ((if def then [(name, setT', NoSyn)] else []) @