1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Jul 28 16:56:14 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Jul 31 11:13:38 2011 -0700
     1.3 @@ -119,28 +119,34 @@
     1.4         non-pcpo-types and invalid use of recursive type
     1.5         replace sorts in type variables on rhs *)
     1.6      val rec_tab = Domain_Take_Proofs.get_rec_tab thy
     1.7 -    fun check_rec rec_ok (T as TFree (v,_))  =
     1.8 +    fun check_rec no_rec (T as TFree (v,_))  =
     1.9          if AList.defined (op =) sorts v then T
    1.10          else error ("Free type variable " ^ quote v ^ " on rhs.")
    1.11 -      | check_rec rec_ok (T as Type (s, Ts)) =
    1.12 +      | check_rec no_rec (T as Type (s, Ts)) =
    1.13          (case AList.lookup (op =) dtnvs' s of
    1.14            NONE =>
    1.15 -            let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s
    1.16 -            in Type (s, map (check_rec rec_ok') Ts) end
    1.17 +            let val no_rec' =
    1.18 +                  if no_rec = NONE then
    1.19 +                    if Symtab.defined rec_tab s then NONE else SOME s
    1.20 +                  else no_rec
    1.21 +            in Type (s, map (check_rec no_rec') Ts) end
    1.22          | SOME typevars =>
    1.23            if typevars <> Ts
    1.24            then error ("Recursion of type " ^ 
    1.25                        quote (Syntax.string_of_typ_global tmp_thy T) ^ 
    1.26                        " with different arguments")
    1.27 -          else if rec_ok then T
    1.28 -          else error ("Illegal indirect recursion of type " ^ 
    1.29 -                      quote (Syntax.string_of_typ_global tmp_thy T)))
    1.30 -      | check_rec rec_ok (TVar _) = error "extender:check_rec"
    1.31 +          else (case no_rec of
    1.32 +                  NONE => T
    1.33 +                | SOME c =>
    1.34 +                  error ("Illegal indirect recursion of type " ^ 
    1.35 +                         quote (Syntax.string_of_typ_global tmp_thy T) ^
    1.36 +                         " under type constructor " ^ quote c)))
    1.37 +      | check_rec no_rec (TVar _) = error "extender:check_rec"
    1.38  
    1.39      fun prep_arg (lazy, sel, raw_T) =
    1.40        let
    1.41          val T = prep_typ tmp_thy sorts raw_T
    1.42 -        val _ = check_rec true T
    1.43 +        val _ = check_rec NONE T
    1.44          val _ = check_pcpo (lazy, sel, T)
    1.45        in (lazy, sel, T) end
    1.46      fun prep_con (b, args, mx) = (b, map prep_arg args, mx)