--- a/src/HOL/Tools/function_package/size.ML Wed Jan 02 15:14:24 2008 +0100
+++ b/src/HOL/Tools/function_package/size.ML Wed Jan 02 15:14:25 2008 +0100
@@ -27,14 +27,6 @@
val lookup_size = SizeData.get #> Symtab.lookup;
-fun instance_size_class tyco thy =
- thy
- |> TheoryTarget.instantiation
- ([tyco], replicate (Sign.arity_number thy tyco) HOLogic.typeS, [HOLogic.class_size])
- |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit
- |> ProofContext.theory_of;
-
fun plus (t1, t2) = Const ("HOL.plus_class.plus",
HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
@@ -137,6 +129,14 @@
Const (rec_name, fTs @ [T] ---> HOLogic.natT))
(recTs ~~ rec_names));
+ fun instance_size_class tyco thy =
+ thy
+ |> TheoryTarget.instantiation
+ ([tyco], replicate (Sign.arity_number thy tyco) HOLogic.typeS, [HOLogic.class_size])
+ |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+ |> LocalTheory.exit
+ |> ProofContext.theory_of;
+
val ((size_def_thms, size_def_thms'), thy') =
thy
|> Sign.add_consts_i (map (fn (s, T) =>