changeset 24346 | 4f6b71b84ee7 |
parent 24218 | fbf1646b267c |
child 24423 | ae9cd0e92423 |
--- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Aug 20 18:07:29 2007 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Aug 20 18:07:30 2007 +0200 @@ -427,8 +427,8 @@ val n = Sign.arity_number thy tyco; in thy - |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size]) - (Class.intro_classes_tac []) + |> Class.prove_instance_arity (Class.intro_classes_tac []) + [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] [] end val (size_def_thms, thy') =