really unfold
authorblanchet
Thu Apr 24 21:00:00 2014 +0200 (2014-04-24)
changeset 56682d39926ff0487
parent 56681 e8d5d60d655e
child 56683 7f4ae504e059
really unfold
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Apr 24 17:52:19 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Apr 24 21:00:00 2014 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4      fun derive_overloaded_size_simp size_def' simp0 =
     1.5        (trans OF [size_def', simp0])
     1.6        |> unfold_thms lthy2 @{thms add_0_left add_0_right}
     1.7 -      |> fold_thms lthy2 overloaded_size_defs';
     1.8 +      |> fold_thms lthy2 overloaded_size_defs;
     1.9  
    1.10      val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
    1.11      val size_simps = flat size_simpss;