diff -r ed9a1254d674 -r d3fca349736c src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Sep 15 19:27:43 2007 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Sep 15 19:27:44 2007 +0200 @@ -427,7 +427,7 @@ val n = Sign.arity_number thy tyco; in thy - |> Class.prove_instance_arity (Class.intro_classes_tac []) + |> Class.prove_instance (Class.intro_classes_tac []) [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] [] |> snd end