changeset 24589 | d3fca349736c |
parent 24423 | ae9cd0e92423 |
child 24699 | c6674504103f |
--- 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