# HG changeset patch
# User haftmann
# Date 1199283265 -3600
# Node ID 850abe253ffc3643bc6825c44219bfa4de9241d4
# Parent  1c1ca4b20ec69de20815c55a19e03f08c2b5caa6
tuned

diff -r 1c1ca4b20ec6 -r 850abe253ffc src/HOL/Tools/function_package/size.ML
--- 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) =>