# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID 16e1fa9d094fd3627c786f06319de2934811b75d
# Parent  2ffa440b30743f9da38074b36102c75babc5e383
put theorems in right slot

diff -r 2ffa440b3074 -r 16e1fa9d094f src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/Function/size.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -207,7 +207,7 @@
 
       in
         fold2 (fn new_type_name => fn size_name =>
-            BNF_LFP_Size.register_size new_type_name size_name [] size_thms)
+            BNF_LFP_Size.register_size new_type_name size_name size_thms [])
           new_type_names size_names thy''
       end
   end;