changeset 3793 | 6e807b50b6c1 |
parent 3768 | 67f4ac759100 |
child 3946 | 34152864655c |
--- a/src/HOL/typedef.ML Mon Oct 06 19:13:29 1997 +0200 +++ b/src/HOL/typedef.ML Mon Oct 06 19:13:55 1997 +0200 @@ -108,7 +108,7 @@ thy |> Theory.add_types [(t, tlen, mx)] - |> Theory.add_arities + |> Theory.add_arities_i [(tname, replicate tlen logicS, logicS), (tname, replicate tlen termS, termS)] |> Theory.add_consts_i