# HG changeset patch
# User blanchet
# Date 1367321921 -7200
# Node ID 087498724486034570311b8e9641ecd4a4956646
# Parent  4d6dcd51dd52378772b6b4024e320529979373a9
lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)

diff -r 4d6dcd51dd52 -r 087498724486 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Tue Apr 30 13:38:41 2013 +0200
@@ -8,21 +8,21 @@
 
 signature BNF_COMP =
 sig
-  val ID_bnf: BNF_Def.BNF
-  val DEADID_bnf: BNF_Def.BNF
+  val ID_bnf: BNF_Def.bnf
+  val DEADID_bnf: BNF_Def.bnf
 
   type unfold_set
   val empty_unfolds: unfold_set
 
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
-    (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context)
+    (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
   val default_comp_sort: (string * sort) list list -> (string * sort) list
   val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
-    (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context ->
-    (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context))
-  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
-    (BNF_Def.BNF * typ list) * local_theory
+    (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
+    (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context))
+  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.bnf -> Proof.context ->
+    (BNF_Def.bnf * typ list) * local_theory
 end;
 
 structure BNF_Comp : BNF_COMP =
diff -r 4d6dcd51dd52 -r 087498724486 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:38:41 2013 +0200
@@ -8,21 +8,21 @@
 
 signature BNF_DEF =
 sig
-  type BNF
+  type bnf
   type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
 
-  val morph_bnf: morphism -> BNF -> BNF
-  val eq_bnf: BNF * BNF -> bool
-  val bnf_of: Proof.context -> string -> BNF option
-  val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
+  val morph_bnf: morphism -> bnf -> bnf
+  val eq_bnf: bnf * bnf -> bool
+  val bnf_of: Proof.context -> string -> bnf option
+  val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
 
-  val name_of_bnf: BNF -> binding
-  val T_of_bnf: BNF -> typ
-  val live_of_bnf: BNF -> int
-  val lives_of_bnf: BNF -> typ list
-  val dead_of_bnf: BNF -> int
-  val deads_of_bnf: BNF -> typ list
-  val nwits_of_bnf: BNF -> int
+  val name_of_bnf: bnf -> binding
+  val T_of_bnf: bnf -> typ
+  val live_of_bnf: bnf -> int
+  val lives_of_bnf: bnf -> typ list
+  val dead_of_bnf: bnf -> int
+  val deads_of_bnf: bnf -> typ list
+  val nwits_of_bnf: bnf -> int
 
   val mapN: string
   val relN: string
@@ -30,59 +30,59 @@
   val mk_setN: int -> string
   val srelN: string
 
-  val map_of_bnf: BNF -> term
-  val sets_of_bnf: BNF -> term list
-  val rel_of_bnf: BNF -> term
+  val map_of_bnf: bnf -> term
+  val sets_of_bnf: bnf -> term list
+  val rel_of_bnf: bnf -> term
 
-  val mk_T_of_bnf: typ list -> typ list -> BNF -> typ
-  val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
-  val mk_map_of_bnf: typ list -> typ list -> typ list -> BNF -> term
-  val mk_rel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
-  val mk_sets_of_bnf: typ list list -> typ list list -> BNF -> term list
-  val mk_srel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
-  val mk_wits_of_bnf: typ list list -> typ list list -> BNF -> (int list * term) list
+  val mk_T_of_bnf: typ list -> typ list -> bnf -> typ
+  val mk_bd_of_bnf: typ list -> typ list -> bnf -> term
+  val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
+  val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
+  val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
+  val mk_srel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
+  val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
 
-  val bd_Card_order_of_bnf: BNF -> thm
-  val bd_Cinfinite_of_bnf: BNF -> thm
-  val bd_Cnotzero_of_bnf: BNF -> thm
-  val bd_card_order_of_bnf: BNF -> thm
-  val bd_cinfinite_of_bnf: BNF -> thm
-  val collect_set_map_of_bnf: BNF -> thm
-  val in_bd_of_bnf: BNF -> thm
-  val in_cong_of_bnf: BNF -> thm
-  val in_mono_of_bnf: BNF -> thm
-  val in_srel_of_bnf: BNF -> thm
-  val map_comp'_of_bnf: BNF -> thm
-  val map_comp_of_bnf: BNF -> thm
-  val map_cong0_of_bnf: BNF -> thm
-  val map_cong_of_bnf: BNF -> thm
-  val map_def_of_bnf: BNF -> thm
-  val map_id'_of_bnf: BNF -> thm
-  val map_id_of_bnf: BNF -> thm
-  val map_wppull_of_bnf: BNF -> thm
-  val map_wpull_of_bnf: BNF -> thm
-  val rel_def_of_bnf: BNF -> thm
-  val rel_eq_of_bnf: BNF -> thm
-  val rel_flip_of_bnf: BNF -> thm
-  val rel_srel_of_bnf: BNF -> thm
-  val set_bd_of_bnf: BNF -> thm list
-  val set_defs_of_bnf: BNF -> thm list
-  val set_map'_of_bnf: BNF -> thm list
-  val set_map_of_bnf: BNF -> thm list
-  val srel_def_of_bnf: BNF -> thm
-  val srel_Gr_of_bnf: BNF -> thm
-  val srel_Id_of_bnf: BNF -> thm
-  val srel_O_of_bnf: BNF -> thm
-  val srel_O_Gr_of_bnf: BNF -> thm
-  val srel_cong_of_bnf: BNF -> thm
-  val srel_converse_of_bnf: BNF -> thm
-  val srel_mono_of_bnf: BNF -> thm
-  val wit_thms_of_bnf: BNF -> thm list
-  val wit_thmss_of_bnf: BNF -> thm list list
+  val bd_Card_order_of_bnf: bnf -> thm
+  val bd_Cinfinite_of_bnf: bnf -> thm
+  val bd_Cnotzero_of_bnf: bnf -> thm
+  val bd_card_order_of_bnf: bnf -> thm
+  val bd_cinfinite_of_bnf: bnf -> thm
+  val collect_set_map_of_bnf: bnf -> thm
+  val in_bd_of_bnf: bnf -> thm
+  val in_cong_of_bnf: bnf -> thm
+  val in_mono_of_bnf: bnf -> thm
+  val in_srel_of_bnf: bnf -> thm
+  val map_comp'_of_bnf: bnf -> thm
+  val map_comp_of_bnf: bnf -> thm
+  val map_cong0_of_bnf: bnf -> thm
+  val map_cong_of_bnf: bnf -> thm
+  val map_def_of_bnf: bnf -> thm
+  val map_id'_of_bnf: bnf -> thm
+  val map_id_of_bnf: bnf -> thm
+  val map_wppull_of_bnf: bnf -> thm
+  val map_wpull_of_bnf: bnf -> thm
+  val rel_def_of_bnf: bnf -> thm
+  val rel_eq_of_bnf: bnf -> thm
+  val rel_flip_of_bnf: bnf -> thm
+  val rel_srel_of_bnf: bnf -> thm
+  val set_bd_of_bnf: bnf -> thm list
+  val set_defs_of_bnf: bnf -> thm list
+  val set_map'_of_bnf: bnf -> thm list
+  val set_map_of_bnf: bnf -> thm list
+  val srel_def_of_bnf: bnf -> thm
+  val srel_Gr_of_bnf: bnf -> thm
+  val srel_Id_of_bnf: bnf -> thm
+  val srel_O_of_bnf: bnf -> thm
+  val srel_O_Gr_of_bnf: bnf -> thm
+  val srel_cong_of_bnf: bnf -> thm
+  val srel_converse_of_bnf: bnf -> thm
+  val srel_mono_of_bnf: bnf -> thm
+  val wit_thms_of_bnf: bnf -> thm list
+  val wit_thmss_of_bnf: bnf -> thm list list
 
   val mk_witness: int list * term -> thm list -> nonemptiness_witness
   val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
-  val wits_of_bnf: BNF -> nonemptiness_witness list
+  val wits_of_bnf: bnf -> nonemptiness_witness list
 
   val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
 
@@ -98,7 +98,7 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
     binding -> binding list ->
     ((((binding * term) * term list) * term) * term list) * term option ->
-    local_theory -> BNF * local_theory
+    local_theory -> bnf * local_theory
 end;
 
 structure BNF_Def : BNF_DEF =
@@ -286,7 +286,7 @@
 fun map_witness f g {I, wit, prop} = {I = I, wit = f wit, prop = map g prop};
 fun morph_witness phi = map_witness (Morphism.term phi) (Morphism.thm phi);
 
-datatype BNF = BNF of {
+datatype bnf = BNF of {
   name: binding,
   T: typ,
   live: int,
@@ -434,7 +434,7 @@
 
 structure Data = Generic_Data
 (
-  type T = BNF Symtab.table;
+  type T = bnf Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   val merge = Symtab.merge eq_bnf;
diff -r 4d6dcd51dd52 -r 087498724486 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 30 13:38:41 2013 +0200
@@ -9,7 +9,7 @@
 signature BNF_FP =
 sig
   type fp_result =
-    {bnfs: BNF_Def.BNF list,
+    {bnfs: BNF_Def.bnf list,
      dtors: term list,
      ctors: term list,
      folds: term list,
@@ -158,10 +158,10 @@
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
   val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
-      binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+      binding list -> binding list 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
+    (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
 end;
 
 structure BNF_FP : BNF_FP =
@@ -172,7 +172,7 @@
 open BNF_Util
 
 type fp_result =
-  {bnfs: BNF_Def.BNF list,
+  {bnfs: BNF_Def.bnf list,
    dtors: term list,
    ctors: term list,
    folds: term list,
diff -r 4d6dcd51dd52 -r 087498724486 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 13:38:41 2013 +0200
@@ -15,14 +15,14 @@
 
   val fp_of: Proof.context -> string -> fp option
 
-  val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> term list -> term list -> thm ->
-    thm list -> thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
+  val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm ->
+    thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
     typ list -> term list list -> thm list list -> term list -> term list -> thm list -> thm list ->
     Proof.context ->
     (thm * thm list * Args.src list) * (thm list list * Args.src list)
     * (thm list list * Args.src list)
-  val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.BNF list -> term list -> term list ->
-    thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list -> BNF_Def.BNF list ->
+  val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list ->
+    thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list ->
     typ list -> typ list -> typ list -> int list list -> int list list -> int list ->
     term list list -> thm list list -> BNF_Ctr_Sugar.ctr_wrap_result list -> term list ->
     term list -> thm list -> thm list -> Proof.context ->
@@ -33,7 +33,7 @@
 
   val datatypes: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
-      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+      binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
       BNF_FP.fp_result * local_theory) ->
     (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
       ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
@@ -41,7 +41,7 @@
     local_theory -> local_theory
   val parse_datatype_cmd: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
-      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+      binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
       BNF_FP.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
 end;
diff -r 4d6dcd51dd52 -r 087498724486 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Apr 30 13:38:41 2013 +0200
@@ -10,7 +10,7 @@
 signature BNF_GFP =
 sig
   val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
-    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+    binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
     local_theory -> BNF_FP.fp_result * local_theory
 end;
 
diff -r 4d6dcd51dd52 -r 087498724486 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Apr 30 13:38:41 2013 +0200
@@ -9,7 +9,7 @@
 signature BNF_LFP =
 sig
   val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
-    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+    binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
     local_theory -> BNF_FP.fp_result * local_theory
 end;