--- a/src/HOL/Tools/inductive_realizer.ML Tue Oct 09 17:10:32 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Oct 09 17:10:34 2007 +0200
@@ -300,7 +300,7 @@
val thy1' = thy1 |>
Theory.copy |>
Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
- fold (fn s => AxClass.axiomatize_arity_i
+ fold (fn s => AxClass.axiomatize_arity
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
val dts = List.mapPartial (fn (s, rs) => if s mem rsets then