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/domain/theorems.ML
changeset 3044 3e3087aa69e7
parent 2446 c2a9bf6c0948
child 3323 194ae2e0c193 
--- a/src/HOLCF/domain/theorems.ML	Thu Apr 24 18:44:32 1997 +0200
+++ b/src/HOLCF/domain/theorems.ML	Thu Apr 24 18:51:14 1997 +0200
@@ -442,7 +442,7 @@
                                   asm_simp_tac take_ss 1 ::
                                   map (fn arg =>
                                    case_UU_tac (prems@con_rews) 1 (
-                           nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
+                           nth_elem(rec_of arg,dnames)^"_take n`"^vname arg))
                                   (filter is_nonlazy_rec args) @ [
                                   resolve_tac prems 1] @
                                   map (K (atac 1))      (nonlazy args) @
isabelle