1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 13:10:34 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 14:51:52 2012 +0200
     1.3 @@ -95,8 +95,11 @@
     1.4  fun args_of ((_, args), _) = args;
     1.5  fun ctr_mixfix_of (_, mx) = mx;
     1.6  
     1.7 -fun prepare_datatype prepare_typ lfp specs fake_lthy no_defs_lthy =
     1.8 +fun prepare_datatype prepare_typ lfp (no_dests, specs) fake_lthy no_defs_lthy =
     1.9    let
    1.10 +    val _ = if not lfp andalso no_dests then error "Cannot use \"no_dests\" option for codatatypes"
    1.11 +      else ();
    1.12 +
    1.13      val constrained_As =
    1.14        map (map (apfst (prepare_typ fake_lthy)) o type_args_constrained_of) specs
    1.15        |> Library.foldr1 (merge_type_args_constrained no_defs_lthy);
    1.16 @@ -477,7 +480,7 @@
    1.17                corec_def), lthy)
    1.18            end;
    1.19        in
    1.20 -        wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy'
    1.21 +        wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, sel_binderss)) lthy'
    1.22          |> (if lfp then some_lfp_sugar else some_gfp_sugar)
    1.23        end;
    1.24  
    1.25 @@ -669,7 +672,7 @@
    1.26      (timer; lthy')
    1.27    end;
    1.28  
    1.29 -fun datatype_cmd info specs lthy =
    1.30 +fun datatype_cmd lfp (bundle as (_, specs)) lthy =
    1.31    let
    1.32      (* TODO: cleaner handling of fake contexts, without "background_theory" *)
    1.33      (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
    1.34 @@ -679,7 +682,7 @@
    1.35          (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
    1.36      val fake_lthy = Proof_Context.background_theory fake_thy lthy;
    1.37    in
    1.38 -    prepare_datatype Syntax.read_typ info specs fake_lthy lthy
    1.39 +    prepare_datatype Syntax.read_typ lfp bundle fake_lthy lthy
    1.40    end;
    1.41  
    1.42  val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
    1.43 @@ -693,12 +696,14 @@
    1.44    (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding --
    1.45      Scan.repeat parse_ctr_arg -- Parse.opt_mixfix));
    1.46  
    1.47 +val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
    1.48 +
    1.49  val _ =
    1.50    Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
    1.51 -    (Parse.and_list1 parse_single_spec >> datatype_cmd true);
    1.52 +    (parse_datatype >> datatype_cmd true);
    1.53  
    1.54  val _ =
    1.55    Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
    1.56 -    (Parse.and_list1 parse_single_spec >> datatype_cmd false);
    1.57 +    (parse_datatype >> datatype_cmd false);
    1.58  
    1.59  end;