src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58364 efc56d935728
parent 58362 cf32eb8001b8
child 58427 cc1bab5558b0
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 23:45:28 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 23:45:57 2014 +0200
     1.3 @@ -61,9 +61,6 @@
     1.4  
     1.5  (* collection of declarations *)
     1.6  
     1.7 -fun declared declss T = exists (exists (equal T o fst)) declss
     1.8 -fun declared' dss T = exists (exists (equal T o fst) o snd) dss
     1.9 -
    1.10  (* Simplification: We assume that every type that is not a codatatype is a datatype (or a
    1.11     record). *)
    1.12  fun fp_kind_of ctxt n =
    1.13 @@ -79,14 +76,16 @@
    1.14        | info :: _ => (get_typedef_decl info T Ts, ctxt))
    1.15    in
    1.16      (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.17 -      SOME ctr_sugar =>
    1.18 +      SOME (ctr_sugar as {T = U as Type (_, Us), ...}) =>
    1.19        if fp_kind_of ctxt n = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else fallback ()
    1.20      | NONE => fallback ())
    1.21    end
    1.22  
    1.23  fun add_decls fp T (declss, ctxt) =
    1.24    let
    1.25 -    fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
    1.26 +    fun declared T = exists (exists (equal T o fst))
    1.27 +    fun declared' T = exists (exists (equal T o fst) o snd)
    1.28 +    fun depends ds = exists (member (op =) (map fst ds))
    1.29  
    1.30      fun add (TFree _) = I
    1.31        | add (TVar _) = I
    1.32 @@ -94,7 +93,7 @@
    1.33            fold add (Term.body_type T :: Term.binder_types T)
    1.34        | add @{typ bool} = I
    1.35        | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
    1.36 -          if declared declss T orelse declared' dss T then (dss, ctxt1)
    1.37 +          if declared T declss orelse declared' T dss then (dss, ctxt1)
    1.38            else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
    1.39            else
    1.40              (case get_decls fp T n Ts ctxt1 of
    1.41 @@ -106,8 +105,7 @@
    1.42  
    1.43                    fun ins [] = [(Us, ds)]
    1.44                      | ins ((Uds as (Us', _)) :: Udss) =
    1.45 -                        if depends Us' ds then (Us, ds) :: Uds :: Udss
    1.46 -                        else Uds :: ins Udss
    1.47 +                        if depends ds Us' then (Us, ds) :: Uds :: Udss else Uds :: ins Udss
    1.48              in fold add Us (ins dss, ctxt2) end))
    1.49    in add T ([], ctxt) |>> append declss o map snd end
    1.50