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/HOL/BNF/Tools/bnf_gfp.ML
changeset 49668 0209087a14d0
parent 49636 b7256a88a84b
child 49833 1d80798e8d8a 
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 30 12:08:16 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 30 22:02:34 2012 +0200
@@ -2698,7 +2698,7 @@
                 Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))
               dtors set_incl_hset_thmss;
 
-            val tinst = interleave (map (SOME o certify lthy) dtors) (replicate n NONE)
+            val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE)
             val set_minimal_thms =
               map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o
                 Drule.zero_var_indexes)
isabelle