src/HOLCF/domain/theorems.ML
changeset 3044 3e3087aa69e7
parent 2446 c2a9bf6c0948
child 3323 194ae2e0c193
     1.1 --- a/src/HOLCF/domain/theorems.ML	Thu Apr 24 18:44:32 1997 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Apr 24 18:51:14 1997 +0200
     1.3 @@ -442,7 +442,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 n1`"^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) @