src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58428 e4e34dfc3e68
parent 58427 cc1bab5558b0
child 58429 0b94858325a5
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:23 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:24 2014 +0200
     1.3 @@ -71,8 +71,23 @@
     1.4        | info :: _ => (get_typedef_decl info T Ts, ctxt))
     1.5    in
     1.6      (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
     1.7 -      SOME {fp = fp', ctr_sugar, ...} =>
     1.8 -      if fp' = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else ([], ctxt)
     1.9 +      SOME {fp = fp', fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
    1.10 +      if fp' = fp then
    1.11 +        let
    1.12 +          val ns = map (fst o dest_Type) fp_Ts
    1.13 +          val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
    1.14 +          val Xs = map #X mutual_fp_sugars
    1.15 +          val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
    1.16 +
    1.17 +          fun is_nested_co_recursive (T as Type _) =
    1.18 +              BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T
    1.19 +            | is_nested_co_recursive _ = false
    1.20 +        in
    1.21 +          if exists (exists (exists is_nested_co_recursive)) ctrXs_Tsss then maybe_typedef ()
    1.22 +          else get_ctr_sugar_decl ctr_sugar T Ts ctxt
    1.23 +        end
    1.24 +      else
    1.25 +        ([], ctxt)
    1.26      | NONE =>
    1.27        if fp = BNF_Util.Least_FP then
    1.28          if String.isSuffix extN n then