src/HOL/Tools/datatype_package.ML
changeset 24218 fbf1646b267c
parent 24098 f1eb34ae33af
child 24346 4f6b71b84ee7
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Aug 10 17:04:20 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Aug 10 17:04:24 2007 +0200
     1.3 @@ -566,7 +566,7 @@
     1.4        in
     1.5          thy
     1.6          |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
     1.7 -             (ClassPackage.intro_classes_tac [])
     1.8 +             (Class.intro_classes_tac [])
     1.9        end
    1.10  
    1.11      val thy2' = thy