src/HOL/Tools/SMT/smt_datatypes.ML
changeset 59020 a86683d6c97e
parent 58634 9f10d82e8188
child 59142 705f8aea8d60
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Thu Nov 20 17:29:18 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Thu Nov 20 17:29:18 2014 +0100
     1.3 @@ -89,8 +89,16 @@
     1.4                forall (if is_same_fp s then is_homogenously_nested_co_recursive
     1.5                  else not o BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs) Ts
     1.6              | is_homogenously_nested_co_recursive _ = true
     1.7 +
     1.8 +          val Type (_, As) :: _ = fp_Ts
     1.9 +          val substAs = Term.typ_subst_atomic (As ~~ Ts);
    1.10          in
    1.11 -          if forall (forall (forall is_homogenously_nested_co_recursive)) ctrXs_Tsss then
    1.12 +          (* TODO/FIXME: The "bool" check is there to work around a CVC4 bug
    1.13 +             (http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=597). It should be removed once
    1.14 +             the bug is fixed. *)
    1.15 +          if forall (forall (forall (is_homogenously_nested_co_recursive))) ctrXs_Tsss andalso
    1.16 +             forall (forall (forall (curry (op <>) @{typ bool})))
    1.17 +               (map (map (map substAs)) ctrXs_Tsss) then
    1.18              get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp)
    1.19            else
    1.20              maybe_typedef ()