1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 20:22:03 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 22:13:22 2012 +0200
     1.3 @@ -7,7 +7,10 @@
     1.4  
     1.5  signature BNF_FP_SUGAR =
     1.6  sig
     1.7 -  (* TODO: programmatic interface *)
     1.8 +  val datatyp: bool ->
     1.9 +    bool * ((((typ * typ option) list * binding) * mixfix) * ((((binding * binding) *
    1.10 +      (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
    1.11 +    local_theory -> local_theory
    1.12  end;
    1.13  
    1.14  structure BNF_FP_Sugar : BNF_FP_SUGAR =
    1.15 @@ -46,7 +49,7 @@
    1.16  
    1.17  fun retype_free (Free (s, _)) T = Free (s, T);
    1.18  
    1.19 -val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs))
    1.20 +val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
    1.21  
    1.22  fun mk_predT T = T --> HOLogic.boolT;
    1.23  
    1.24 @@ -145,9 +148,9 @@
    1.25        | A' :: _ => error ("Extra type variables on rhs: " ^
    1.26            quote (Syntax.string_of_typ no_defs_lthy (TFree A'))));
    1.27  
    1.28 -    val ((Cs, Xs), _) =
    1.29 +    val ((Bs, Cs), _) =
    1.30        no_defs_lthy
    1.31 -      |> fold (fold (fn s => Variable.declare_typ (TFree (s, dummyS))) o type_args_of) specs
    1.32 +      |> fold Variable.declare_typ As
    1.33        |> mk_TFrees N
    1.34        ||>> mk_TFrees N;
    1.35  
    1.36 @@ -157,13 +160,13 @@
    1.37        | eq_fpT _ _ = false;
    1.38  
    1.39      fun freeze_fp (T as Type (s, Us)) =
    1.40 -        (case find_index (eq_fpT T) fakeTs of ~1 => Type (s, map freeze_fp Us) | j => nth Xs j)
    1.41 +        (case find_index (eq_fpT T) fakeTs of ~1 => Type (s, map freeze_fp Us) | j => nth Bs j)
    1.42        | freeze_fp T = T;
    1.43  
    1.44 -    val ctr_TsssXs = map (map (map freeze_fp)) fake_ctr_Tsss;
    1.45 -    val ctr_sum_prod_TsXs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssXs;
    1.46 +    val ctr_TsssBs = map (map (map freeze_fp)) fake_ctr_Tsss;
    1.47 +    val ctr_sum_prod_TsBs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssBs;
    1.48  
    1.49 -    val eqs = map dest_TFree Xs ~~ ctr_sum_prod_TsXs;
    1.50 +    val eqs = map dest_TFree Bs ~~ ctr_sum_prod_TsBs;
    1.51  
    1.52      val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
    1.53          fp_iter_thms, fp_rec_thms), lthy)) =
    1.54 @@ -179,7 +182,7 @@
    1.55        in snd oo add end;
    1.56  
    1.57      val nested_bnfs =
    1.58 -      map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
    1.59 +      map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssBs []);
    1.60  
    1.61      val timer = time (Timer.startRealTimer ());
    1.62  
    1.63 @@ -196,7 +199,7 @@
    1.64  
    1.65      val fpTs = map (domain_type o fastype_of) unfs;
    1.66  
    1.67 -    val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctr_TsssXs;
    1.68 +    val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs;
    1.69      val ns = map length ctr_Tsss;
    1.70      val kss = map (fn n => 1 upto n) ns;
    1.71      val mss = map (map length) ctr_Tsss;
    1.72 @@ -685,6 +688,8 @@
    1.73      (timer; lthy')
    1.74    end;
    1.75  
    1.76 +fun datatyp lfp bundle lthy = prepare_datatype (K I) (K I) lfp bundle lthy lthy;
    1.77 +
    1.78  fun datatype_cmd lfp (bundle as (_, specs)) lthy =
    1.79    let
    1.80      (* TODO: cleaner handling of fake contexts, without "background_theory" *)

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 11 20:22:03 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 11 22:13:22 2012 +0200
     2.3 @@ -572,6 +572,10 @@
     2.4    map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
     2.5    |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
     2.6  
     2.7 +val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
     2.8 +  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
     2.9 +  prepare_wrap_datatype Syntax.read_term;
    2.10 +
    2.11  fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
    2.12  
    2.13  val parse_bindings = parse_bracket_list Parse.binding;
    2.14 @@ -581,10 +585,6 @@
    2.15  val parse_bound_terms = parse_bracket_list parse_bound_term;
    2.16  val parse_bound_termss = parse_bracket_list parse_bound_terms;
    2.17  
    2.18 -val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
    2.19 -  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    2.20 -  prepare_wrap_datatype Syntax.read_term;
    2.21 -
    2.22  val parse_wrap_options =
    2.23    Scan.optional (@{keyword "("} |-- (@{keyword "no_dests"} >> K true) --| @{keyword ")"}) false;
    2.24