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) @