# HG changeset patch # User wenzelm # Date 1323873017 -3600 # Node ID afdb92130f5a4131dd0305a33583397dd00bb8e5 # Parent fcb897b39fa318115b4bf2b17ca87773f236a6a6 tuned signature; diff -r fcb897b39fa3 -r afdb92130f5a src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Dec 14 12:18:19 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Dec 14 15:30:17 2011 +0100 @@ -6,7 +6,8 @@ signature NOMINAL_DATATYPE = sig - val add_nominal_datatype : Datatype.config -> Datatype.spec_cmd list -> theory -> theory + val nominal_datatype : Datatype.config -> Datatype.spec list -> theory -> theory + val nominal_datatype_cmd : Datatype.config -> Datatype.spec_cmd list -> theory -> theory type descr type nominal_datatype_info val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table @@ -185,7 +186,7 @@ fun fresh_star_const T U = Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT); -fun gen_add_nominal_datatype prep_specs config dts thy = +fun gen_nominal_datatype prep_specs config dts thy = let val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts; @@ -2065,11 +2066,12 @@ thy13 end; -val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_specs; +val nominal_datatype = gen_nominal_datatype Datatype.check_specs; +val nominal_datatype_cmd = gen_nominal_datatype Datatype.read_specs; val _ = - Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl - (Parse.and_list1 Datatype.spec_cmd - >> (Toplevel.theory o add_nominal_datatype Datatype.default_config)); + Outer_Syntax.command "nominal_datatype" "define nominal datatypes" Keyword.thy_decl + (Parse.and_list1 Datatype.spec_cmd >> + (Toplevel.theory o nominal_datatype_cmd Datatype.default_config)); end diff -r fcb897b39fa3 -r afdb92130f5a src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Dec 14 12:18:19 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Dec 14 15:30:17 2011 +0100 @@ -19,7 +19,7 @@ val read_specs: spec_cmd list -> theory -> spec list * Proof.context val check_specs: spec list -> theory -> spec list * Proof.context val add_datatype: config -> spec list -> theory -> string list * theory - val add_datatype_cmd: spec_cmd list -> theory -> theory + val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory val spec_cmd: spec_cmd parser end; @@ -798,7 +798,7 @@ end; val add_datatype = gen_add_datatype check_specs; -val add_datatype_cmd = snd oo gen_add_datatype read_specs Datatype_Aux.default_config; +val add_datatype_cmd = gen_add_datatype read_specs; (* outer syntax *) @@ -810,7 +810,8 @@ val _ = Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl - (Parse.and_list1 spec_cmd >> (Toplevel.theory o add_datatype_cmd)); + (Parse.and_list1 spec_cmd + >> (Toplevel.theory o (snd oo add_datatype_cmd Datatype_Aux.default_config))); open Datatype_Data;