# HG changeset patch
# User wenzelm
# Date 1350850298 -7200
# Node ID 4d84fe96d5cb83826a2f5ebbf9be8708a0b56763
# Parent  326f87427719856afb9702c35c5207bde240a22c
tuned;

diff -r 326f87427719 -r 4d84fe96d5cb src/HOL/Tools/Function/size.ML
--- 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;