--- a/src/HOL/Tools/Function/size.ML Sun Oct 21 17:04:13 2012 +0200
+++ b/src/HOL/Tools/Function/size.ML Sun Oct 21 22:11:38 2012 +0200
@@ -13,7 +13,7 @@
structure Size: SIZE =
struct
-structure SizeData = Theory_Data
+structure Data = Theory_Data
(
type T = (string * thm list) Symtab.table;
val empty = Symtab.empty;
@@ -21,7 +21,7 @@
fun merge data = Symtab.merge (K true) data;
);
-val lookup_size = SizeData.get #> Symtab.lookup;
+val lookup_size = Data.get #> Symtab.lookup;
fun plus (t1, t2) = Const (@{const_name Groups.plus},
HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
@@ -210,7 +210,7 @@
[(size_eqns, [])])];
in
- SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
+ Data.map (fold (Symtab.update_new o apsnd (rpair size_thms))
(new_type_names ~~ size_names)) thy''
end;