1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 02:06:31 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 05:03:18 2012 +0200
     1.3 @@ -8,9 +8,19 @@
     1.4  signature BNF_FP_SUGAR =
     1.5  sig
     1.6    val datatyp: bool ->
     1.7 +    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
     1.8 +      BNF_Def.BNF list -> local_theory ->
     1.9 +      (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
    1.10 +         thm list) * local_theory) ->
    1.11      bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
    1.12        (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
    1.13      local_theory -> local_theory
    1.14 +  val parse_datatype_cmd: bool ->
    1.15 +    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
    1.16 +      BNF_Def.BNF list -> local_theory ->
    1.17 +      (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
    1.18 +         thm list) * local_theory) ->
    1.19 +    (local_theory -> local_theory) parser
    1.20  end;
    1.21  
    1.22  structure BNF_FP_Sugar : BNF_FP_SUGAR =
    1.23 @@ -20,8 +30,6 @@
    1.24  open BNF_Wrap
    1.25  open BNF_Def
    1.26  open BNF_FP_Util
    1.27 -open BNF_LFP
    1.28 -open BNF_GFP
    1.29  open BNF_FP_Sugar_Tactics
    1.30  
    1.31  val caseN = "case";
    1.32 @@ -79,7 +87,6 @@
    1.33    if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
    1.34  
    1.35  fun type_args_constrained_of (((cAs, _), _), _) = cAs;
    1.36 -val type_args_of = map fst o type_args_constrained_of;
    1.37  fun type_binder_of (((_, b), _), _) = b;
    1.38  fun mixfix_of ((_, mx), _) = mx;
    1.39  fun ctr_specs_of (_, ctr_specs) = ctr_specs;
    1.40 @@ -90,7 +97,7 @@
    1.41  fun defaults_of ((_, ds), _) = ds;
    1.42  fun ctr_mixfix_of (_, mx) = mx;
    1.43  
    1.44 -fun define_datatype prepare_constraint prepare_typ prepare_term lfp (no_dests, specs)
    1.45 +fun define_datatype prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs)
    1.46      no_defs_lthy0 =
    1.47    let
    1.48      (* TODO: sanity checks on arguments *)
    1.49 @@ -148,7 +155,7 @@
    1.50      val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
    1.51      val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
    1.52  
    1.53 -    val (Ass as As :: _) :: fake_ctr_Tsss =
    1.54 +    val (As :: _) :: fake_ctr_Tsss =
    1.55        burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
    1.56  
    1.57      val _ = (case duplicates (op =) unsorted_As of [] => ()
    1.58 @@ -178,8 +185,7 @@
    1.59  
    1.60      val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
    1.61          fp_iter_thms, fp_rec_thms), lthy)) =
    1.62 -      fp_bnf (if lfp then bnf_lfp else bnf_gfp) fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs
    1.63 -        no_defs_lthy0;
    1.64 +      fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    1.65  
    1.66      val add_nested_bnf_names =
    1.67        let
    1.68 @@ -694,7 +700,7 @@
    1.69      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
    1.70        (if lfp then "" else "co") ^ "datatype"));
    1.71    in
    1.72 -    (timer; lthy')
    1.73 +    timer; lthy'
    1.74    end;
    1.75  
    1.76  val datatyp = define_datatype (K I) (K I) (K I);
    1.77 @@ -717,12 +723,6 @@
    1.78  
    1.79  val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
    1.80  
    1.81 -val _ =
    1.82 -  Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
    1.83 -    (parse_datatype >> datatype_cmd true);
    1.84 -
    1.85 -val _ =
    1.86 -  Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
    1.87 -    (parse_datatype >> datatype_cmd false);
    1.88 +fun parse_datatype_cmd lfp construct = parse_datatype >> datatype_cmd lfp construct;
    1.89  
    1.90  end;