--- 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;