# HG changeset patch
# User haftmann
# Date 1187626050 -7200
# Node ID 4f6b71b84ee7902c13db44502b7464326963cdae
# Parent  86a3557a9ebbd9a9cb3f9f95e4ee7b6ef4a56ebb
using canonical instantiation interface

diff -r 86a3557a9ebb -r 4f6b71b84ee7 src/HOL/Tools/datatype_abs_proofs.ML
--- 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') =
diff -r 86a3557a9ebb -r 4f6b71b84ee7 src/HOL/Tools/datatype_package.ML
--- 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