Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Tools/fixrec.ML
changeset 32952 aeb1e44fbc19
parent 32149 ef59550a55d3
child 33004 715566791eb0 
--- a/src/HOLCF/Tools/fixrec.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -371,7 +371,7 @@
       val simps1 : (Attrib.binding * thm list) list =
         map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
       val simps2 : (Attrib.binding * thm list) list =
-        map (apsnd (fn thm => [thm])) (List.concat simps);
+        map (apsnd (fn thm => [thm])) (flat simps);
       val (_, lthy'') = lthy'
         |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
     in
isabelle