1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:16:28 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:25:44 2013 +0200
     1.3 @@ -51,15 +51,15 @@
     1.4      * (thm list list * thm list list * Args.src list)
     1.5  
     1.6    val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list ->
     1.7 -      binding list list -> (string * sort) list option -> typ list * typ list list ->
     1.8 -      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     1.9 +      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.10 +      local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.11      (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
    1.12        ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    1.13          mixfix) list) list ->
    1.14      local_theory -> local_theory
    1.15    val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list -> binding list ->
    1.16 -      binding list list -> (string * sort) list option -> typ list * typ list list ->
    1.17 -      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.18 +      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.19 +      local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.20      (local_theory -> local_theory) parser
    1.21  end;
    1.22  

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:16:28 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:25:44 2013 +0200
     2.3 @@ -166,8 +166,7 @@
     2.4    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
     2.5  
     2.6    val fp_bnf: (mixfix list -> binding list -> binding list -> binding list -> binding list list ->
     2.7 -      (string * sort) list option -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
     2.8 -      'a) ->
     2.9 +      (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) ->
    2.10      binding list -> mixfix list -> binding list -> binding list -> binding list list ->
    2.11      (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
    2.12  end;
    2.13 @@ -461,13 +460,10 @@
    2.14  
    2.15  (* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
    2.16     also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
    2.17 -fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
    2.18 -    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss
    2.19 -  | fp_sort lhss (SOME resBs) Ass =
    2.20 +fun fp_sort lhss resBs Ass =
    2.21      (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
    2.22  
    2.23 -fun mk_fp_bnf timer construct_fp resBs bs map_bs rel_bs set_bss sort lhss bnfs deadss livess
    2.24 -    unfold_set lthy =
    2.25 +fun mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs deadss livess unfold_set lthy =
    2.26    let
    2.27      val name = mk_common_name (map Binding.name_of bs);
    2.28      fun qualify i =
    2.29 @@ -475,7 +471,7 @@
    2.30        in Binding.qualify true namei end;
    2.31  
    2.32      val Ass = map (map dest_TFree) livess;
    2.33 -    val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
    2.34 +    val resDs = fold (subtract (op =)) Ass resBs;
    2.35      val Ds = fold (fold Term.add_tfreesT) deadss [];
    2.36  
    2.37      val _ = (case Library.inter (op =) Ds lhss of [] => ()
    2.38 @@ -495,7 +491,7 @@
    2.39  
    2.40      val timer = time (timer "Normalization & sealing of BNFs");
    2.41  
    2.42 -    val res = construct_fp bs map_bs rel_bs set_bss resBs (map TFree resDs, deadss) pre_bnfs lthy'';
    2.43 +    val res = construct_fp resBs (map TFree resDs, deadss) pre_bnfs lthy'';
    2.44  
    2.45      val timer = time (timer "FP construction in total");
    2.46    in
    2.47 @@ -506,14 +502,14 @@
    2.48    let
    2.49      val timer = time (Timer.startRealTimer ());
    2.50      val (lhss, rhss) = split_list eqs;
    2.51 -    val sort = fp_sort lhss (SOME resBs);
    2.52 +    val sort = fp_sort lhss resBs;
    2.53      fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
    2.54      val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list)
    2.55        (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
    2.56          (empty_unfolds, lthy));
    2.57    in
    2.58 -    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs rel_bs set_bss sort lhss bnfs Dss
    2.59 -      Ass unfold_set lthy'
    2.60 +    mk_fp_bnf timer (construct_fp mixfixes bs map_bs rel_bs set_bss) resBs bs sort lhss bnfs Dss Ass
    2.61 +      unfold_set lthy'
    2.62    end;
    2.63  
    2.64  end;

     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:16:28 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:25:44 2013 +0200
     3.3 @@ -10,8 +10,8 @@
     3.4  signature BNF_GFP =
     3.5  sig
     3.6    val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
     3.7 -    binding list list -> (string * sort) list option -> typ list * typ list list ->
     3.8 -    BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory
     3.9 +    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    3.10 +    local_theory -> BNF_FP_Util.fp_result * local_theory
    3.11  end;
    3.12  
    3.13  structure BNF_GFP : BNF_GFP =
    3.14 @@ -94,11 +94,9 @@
    3.15      val allCs' = passiveBs @ activeCs;
    3.16      val Css' = replicate n allCs';
    3.17  
    3.18 -    (* typs *)
    3.19 +    (* types *)
    3.20      val dead_poss =
    3.21 -      (case resBs of
    3.22 -        NONE => map SOME deads @ replicate m NONE
    3.23 -      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
    3.24 +      map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs;
    3.25      fun mk_param NONE passive = (hd passive, tl passive)
    3.26        | mk_param (SOME a) passive = (a, passive);
    3.27      val mk_params = fold_map mk_param dead_poss #> fst;

     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:16:28 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:25:44 2013 +0200
     4.3 @@ -9,8 +9,8 @@
     4.4  signature BNF_LFP =
     4.5  sig
     4.6    val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
     4.7 -    binding list list -> (string * sort) list option -> typ list * typ list list ->
     4.8 -    BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory
     4.9 +    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    4.10 +    local_theory -> BNF_FP_Util.fp_result * local_theory
    4.11  end;
    4.12  
    4.13  structure BNF_LFP : BNF_LFP =
    4.14 @@ -61,11 +61,9 @@
    4.15      val allCs' = passiveBs @ activeCs;
    4.16      val Css' = replicate n allCs';
    4.17  
    4.18 -    (* typs *)
    4.19 +    (* types *)
    4.20      val dead_poss =
    4.21 -      (case resBs of
    4.22 -        NONE => map SOME deads @ replicate m NONE
    4.23 -      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
    4.24 +      map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs;
    4.25      fun mk_param NONE passive = (hd passive, tl passive)
    4.26        | mk_param (SOME a) passive = (a, passive);
    4.27      val mk_params = fold_map mk_param dead_poss #> fst;