# HG changeset patch
# User blanchet
# Date 1398366000 -7200
# Node ID d39926ff04878a47d4c17b8f3411d0731d4548ff
# Parent  e8d5d60d655ec790037947d7d9961a5f72623468
really unfold

diff -r e8d5d60d655e -r d39926ff0487 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Apr 24 17:52:19 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Apr 24 21:00:00 2014 +0200
@@ -228,7 +228,7 @@
     fun derive_overloaded_size_simp size_def' simp0 =
       (trans OF [size_def', simp0])
       |> unfold_thms lthy2 @{thms add_0_left add_0_right}
-      |> fold_thms lthy2 overloaded_size_defs';
+      |> fold_thms lthy2 overloaded_size_defs;
 
     val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
     val size_simps = flat size_simpss;