src/HOL/HOLCF/Tools/Domain/domain_induction.ML
changeset 42364 8c674b3b8e44
parent 42361 23f352990944
child 42375 774df7c59508
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Apr 16 16:37:21 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Apr 16 18:11:20 2011 +0200
     1.3 @@ -386,11 +386,11 @@
     1.4          is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
     1.5          ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse 
     1.6            rec_of arg <> n andalso rec_to (rec_of arg::ns) 
     1.7 -            (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
     1.8 +            (lazy_rec orelse is_lazy arg) (n, nth conss (rec_of arg)))
     1.9          ) o snd) cons
    1.10    fun warn (n,cons) =
    1.11      if rec_to [] false (n,cons)
    1.12 -    then (warning ("domain "^List.nth(dnames,n)^" is empty!") true)
    1.13 +    then (warning ("domain " ^ nth dnames n ^ " is empty!") true)
    1.14      else false
    1.15  in
    1.16    val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs