--- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Aug 20 18:07:29 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Aug 20 18:07:30 2007 +0200
@@ -427,8 +427,8 @@
val n = Sign.arity_number thy tyco;
in
thy
- |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
- (Class.intro_classes_tac [])
+ |> Class.prove_instance_arity (Class.intro_classes_tac [])
+ [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
end
val (size_def_thms, thy') =
--- a/src/HOL/Tools/datatype_package.ML Mon Aug 20 18:07:29 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Mon Aug 20 18:07:30 2007 +0200
@@ -565,8 +565,8 @@
val n = Sign.arity_number thy tyco;
in
thy
- |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
- (Class.intro_classes_tac [])
+ |> Class.prove_instance_arity (Class.intro_classes_tac [])
+ [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
end
val thy2' = thy