# HG changeset patch
# User haftmann
# Date 1196860571 -3600
# Node ID 8b7ed8aef0011418c0739c657297150cf1c9bf62
# Parent  58e8ba3b792ba2969a3dace149664eb8bd9fa7a5
canonical instantiation

diff -r 58e8ba3b792b -r 8b7ed8aef001 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Wed Dec 05 14:16:05 2007 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Wed Dec 05 14:16:11 2007 +0100
@@ -33,15 +33,9 @@
 val size_name_base = NameSpace.base size_name;
 val size_suffix = "_" ^ size_name_base;
 
-fun instance_size_class tyco thy =
-  let
-    val n = Sign.arity_number thy tyco;
-  in
-    thy
-    |> Instance.prove_instance (Class.intro_classes_tac [])
-        [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
-    |> snd
-  end
+fun instance_size_class tyco thy = thy |> Instance.instantiate
+  ([tyco], replicate (Sign.arity_number thy tyco) HOLogic.typeS, [HOLogic.class_size])
+    (pair ()) ((K o K) (Class.intro_classes_tac []));
 
 fun plus (t1, t2) = Const ("HOL.plus_class.plus",
   HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;