Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
really unfold
authorblanchet
Thu, 24 Apr 2014 21:00:00 +0200
changeset 56682 d39926ff0487
parent 56681 e8d5d60d655e
child 56683 7f4ae504e059
really unfold
src/HOL/Tools/BNF/bnf_lfp_size.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle