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