src/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 58129 3ec65a7f2b50
parent 58126 3831312eb476
child 58130 5e9170812356
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 16:34:40 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 17:34:03 2014 +0200
     1.3 @@ -15,12 +15,11 @@
     1.4    val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table
     1.5    val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option
     1.6    val the_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info
     1.7 -  val the_spec: theory -> nesting_preference -> string ->
     1.8 -    (string * sort) list * (string * typ list) list
     1.9 +  val the_spec: theory -> string -> (string * sort) list * (string * typ list) list
    1.10    val the_descr: theory -> nesting_preference -> string list ->
    1.11      Old_Datatype_Aux.descr * (string * sort) list * string list * string
    1.12      * (string list * string list) * (typ list * typ list)
    1.13 -  val get_constrs: theory -> nesting_preference -> string -> (string * typ) list option
    1.14 +  val get_constrs: theory -> string -> (string * typ) list option
    1.15    val interpretation: nesting_preference ->
    1.16      (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
    1.17    val datatype_compat: string list -> local_theory -> local_theory
    1.18 @@ -178,7 +177,9 @@
    1.19        #5 (mk_infos_of_mutually_recursive_new_datatypes nesting_pref false subset [fpT_name] lthy);
    1.20    in
    1.21      infos_of nesting_pref
    1.22 -    handle ERROR _ => if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else []
    1.23 +    handle ERROR _ =>
    1.24 +      (if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else [])
    1.25 +      handle ERROR _ => []
    1.26    end;
    1.27  
    1.28  fun get_all thy nesting_pref =
    1.29 @@ -213,13 +214,13 @@
    1.30      SOME info => info
    1.31    | NONE => error ("Unknown datatype " ^ quote T_name));
    1.32  
    1.33 -fun the_spec thy nesting_pref T_name =
    1.34 +fun the_spec thy T_name =
    1.35    let
    1.36 -    val {descr, index, ...} = the_info thy nesting_pref T_name;
    1.37 +    val {descr, index, ...} = the_info thy Keep_Nesting T_name;
    1.38      val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
    1.39 -    val Ts = map Old_Datatype_Aux.dest_DtTFree Ds;
    1.40 +    val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds;
    1.41      val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
    1.42 -  in (Ts, ctrs) end;
    1.43 +  in (tfrees, ctrs) end;
    1.44  
    1.45  fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) =
    1.46    let
    1.47 @@ -253,8 +254,8 @@
    1.48      (descr, vs, T_names, prefix, (names, auxnames), (Ts, Us))
    1.49    end;
    1.50  
    1.51 -fun get_constrs thy nesting_pref T_name =
    1.52 -  try (the_spec thy nesting_pref) T_name
    1.53 +fun get_constrs thy T_name =
    1.54 +  try (the_spec thy) T_name
    1.55    |> Option.map (fn (tfrees, ctrs) =>
    1.56      let
    1.57        fun varify_tfree (s, S) = TVar ((s, 0), S);