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 10835 f4745d77e620
parent 10230 5eb935d6cc69
child 11531 d038246a62f2 
--- a/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -451,7 +451,7 @@
                                   asm_simp_tac take_ss 1 ::
                                   map (fn arg =>
                                    case_UU_tac (prems@con_rews) 1 (
-                           nth_elem(rec_of arg,dnames)^"_take n`"^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