src/HOL/Tools/datatype_package.ML
changeset 24589 d3fca349736c
parent 24423 ae9cd0e92423
child 24624 b8383b1bbae3
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:43 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:44 2007 +0200
     1.3 @@ -565,7 +565,7 @@
     1.4          val n = Sign.arity_number thy tyco;
     1.5        in
     1.6          thy
     1.7 -        |> Class.prove_instance_arity (Class.intro_classes_tac [])
     1.8 +        |> Class.prove_instance (Class.intro_classes_tac [])
     1.9              [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    1.10          |> snd
    1.11        end