| changeset 24926 | bcb6b098df11 |
| parent 24920 | 2a45e400fdad |
| child 25458 | ba8f5e4fa336 |
--- a/src/HOL/Tools/typedef_package.ML Tue Oct 09 17:10:32 2007 +0200 +++ b/src/HOL/Tools/typedef_package.ML Tue Oct 09 17:10:34 2007 +0200 @@ -48,7 +48,7 @@ (** type declarations **) fun HOL_arity (raw_name, args, mx) thy = - thy |> AxClass.axiomatize_arity_i + thy |> AxClass.axiomatize_arity (Sign.full_name thy (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);