src/HOLCF/domain/theorems.ML
changeset 10835 f4745d77e620
parent 10230 5eb935d6cc69
child 11531 d038246a62f2
     1.1 --- a/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -451,7 +451,7 @@
     1.4                                    asm_simp_tac take_ss 1 ::
     1.5                                    map (fn arg =>
     1.6                                     case_UU_tac (prems@con_rews) 1 (
     1.7 -                           nth_elem(rec_of arg,dnames)^"_take n`"^vname arg))
     1.8 +                           nth_elem(rec_of arg,dnames)^"_take n$"^vname arg))
     1.9                                    (filter is_nonlazy_rec args) @ [
    1.10                                    resolve_tac prems 1] @
    1.11                                    map (K (atac 1))      (nonlazy args) @