# HG changeset patch
# User blanchet
# Date 1367511944 -7200
# Node ID 142a828838310c7249d63fc7174b3514d7708483
# Parent  55099e63c5ca59a746e75acdec14041ff7d6f1cd
removed dead code

diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:16:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:25:44 2013 +0200
@@ -51,15 +51,15 @@
     * (thm list list * thm list list * Args.src list)
 
   val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list ->
-      binding list list -> (string * sort) list option -> typ list * typ list list ->
-      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
+      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+      local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
       ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
         mixfix) list) list ->
     local_theory -> local_theory
   val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list -> binding list ->
-      binding list list -> (string * sort) list option -> typ list * typ list list ->
-      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
+      binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+      local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
 end;
 
diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:16:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:25:44 2013 +0200
@@ -166,8 +166,7 @@
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
   val fp_bnf: (mixfix list -> binding list -> binding list -> binding list -> binding list list ->
-      (string * sort) list option -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
-      'a) ->
+      (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) ->
     binding list -> mixfix list -> binding list -> binding list -> binding list list ->
     (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
 end;
@@ -461,13 +460,10 @@
 
 (* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
    also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
-fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
-    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss
-  | fp_sort lhss (SOME resBs) Ass =
+fun fp_sort lhss resBs Ass =
     (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
 
-fun mk_fp_bnf timer construct_fp resBs bs map_bs rel_bs set_bss sort lhss bnfs deadss livess
-    unfold_set lthy =
+fun mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs deadss livess unfold_set lthy =
   let
     val name = mk_common_name (map Binding.name_of bs);
     fun qualify i =
@@ -475,7 +471,7 @@
       in Binding.qualify true namei end;
 
     val Ass = map (map dest_TFree) livess;
-    val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
+    val resDs = fold (subtract (op =)) Ass resBs;
     val Ds = fold (fold Term.add_tfreesT) deadss [];
 
     val _ = (case Library.inter (op =) Ds lhss of [] => ()
@@ -495,7 +491,7 @@
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct_fp bs map_bs rel_bs set_bss resBs (map TFree resDs, deadss) pre_bnfs lthy'';
+    val res = construct_fp resBs (map TFree resDs, deadss) pre_bnfs lthy'';
 
     val timer = time (timer "FP construction in total");
   in
@@ -506,14 +502,14 @@
   let
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
-    val sort = fp_sort lhss (SOME resBs);
+    val sort = fp_sort lhss resBs;
     fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
     val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
         (empty_unfolds, lthy));
   in
-    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs rel_bs set_bss sort lhss bnfs Dss
-      Ass unfold_set lthy'
+    mk_fp_bnf timer (construct_fp mixfixes bs map_bs rel_bs set_bss) resBs bs sort lhss bnfs Dss Ass
+      unfold_set lthy'
   end;
 
 end;
diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:16:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:25:44 2013 +0200
@@ -10,8 +10,8 @@
 signature BNF_GFP =
 sig
   val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
-    binding list list -> (string * sort) list option -> typ list * typ list list ->
-    BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory
+    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+    local_theory -> BNF_FP_Util.fp_result * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -94,11 +94,9 @@
     val allCs' = passiveBs @ activeCs;
     val Css' = replicate n allCs';
 
-    (* typs *)
+    (* types *)
     val dead_poss =
-      (case resBs of
-        NONE => map SOME deads @ replicate m NONE
-      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
+      map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs;
     fun mk_param NONE passive = (hd passive, tl passive)
       | mk_param (SOME a) passive = (a, passive);
     val mk_params = fold_map mk_param dead_poss #> fst;
diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:16:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:25:44 2013 +0200
@@ -9,8 +9,8 @@
 signature BNF_LFP =
 sig
   val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
-    binding list list -> (string * sort) list option -> typ list * typ list list ->
-    BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory
+    binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+    local_theory -> BNF_FP_Util.fp_result * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -61,11 +61,9 @@
     val allCs' = passiveBs @ activeCs;
     val Css' = replicate n allCs';
 
-    (* typs *)
+    (* types *)
     val dead_poss =
-      (case resBs of
-        NONE => map SOME deads @ replicate m NONE
-      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
+      map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs;
     fun mk_param NONE passive = (hd passive, tl passive)
       | mk_param (SOME a) passive = (a, passive);
     val mk_params = fold_map mk_param dead_poss #> fst;