src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 54006 9fe1bd54d437
parent 53974 612505263257
child 54030 732b53d9b720
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 01 12:53:24 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4       nesting_bnfs: BNF_Def.bnf list,
     1.5       fp_res: BNF_FP_Util.fp_result,
     1.6       ctr_defss: thm list list,
     1.7 -     ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
     1.8 +     ctr_sugars: Ctr_Sugar.ctr_sugar list,
     1.9       co_iterss: term list list,
    1.10       mapss: thm list list,
    1.11       co_inducts: thm list,
    1.12 @@ -87,7 +87,7 @@
    1.13      string * term list * term list list * ((term list list * term list list list)
    1.14        * (typ list * typ list list)) list ->
    1.15      thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
    1.16 -    int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list ->
    1.17 +    int list list -> int list list -> int list -> thm list list -> Ctr_Sugar.ctr_sugar list ->
    1.18      term list list -> thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
    1.19    val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.20        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    1.21 @@ -105,8 +105,8 @@
    1.22  structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR =
    1.23  struct
    1.24  
    1.25 +open Ctr_Sugar
    1.26  open BNF_Util
    1.27 -open BNF_Ctr_Sugar
    1.28  open BNF_Comp
    1.29  open BNF_Def
    1.30  open BNF_FP_Util