# HG changeset patch # User huffman # Date 1287888993 25200 # Node ID 429cd74f795f8781d660863204f3b1a2fda0097e # Parent 4d1a8fa8cdfd09eeffdc8ea768ed3986cfd79bba remove legacy comp_dbind option from domain package diff -r 4d1a8fa8cdfd -r 429cd74f795f src/HOLCF/Tools/Domain/domain.ML --- a/src/HOLCF/Tools/Domain/domain.ML Sat Oct 23 11:04:26 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain.ML Sat Oct 23 19:56:33 2010 -0700 @@ -8,25 +8,21 @@ signature DOMAIN = sig val add_domain_cmd: - binding -> ((string * string option) list * binding * mixfix * (binding * (bool * binding option * string) list * mixfix) list) list -> theory -> theory val add_domain: - binding -> ((string * string option) list * binding * mixfix * (binding * (bool * binding option * typ) list * mixfix) list) list -> theory -> theory val add_new_domain_cmd: - binding -> ((string * string option) list * binding * mixfix * (binding * (bool * binding option * string) list * mixfix) list) list -> theory -> theory val add_new_domain: - binding -> ((string * string option) list * binding * mixfix * (binding * (bool * binding option * typ) list * mixfix) list) list -> theory -> theory @@ -50,7 +46,6 @@ (prep_typ : theory -> (string * sort) list -> 'a -> typ) (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory) (arg_sort : bool -> sort) - (comp_dbind : binding) (raw_specs : ((string * string option) list * binding * mixfix * (binding * (bool * binding option * 'a) list * mixfix) list) list) (thy : theory) = @@ -172,7 +167,7 @@ (dbinds ~~ rhss ~~ iso_infos); val (take_rews, thy) = - Domain_Induction.comp_theorems comp_dbind + Domain_Induction.comp_theorems dbinds take_info constr_infos thy; in thy @@ -240,27 +235,21 @@ (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl); val domains_decl = - Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") -- - Parse.and_list1 domain_decl; + Parse.and_list1 domain_decl; fun mk_domain (definitional : bool) - (opt_name : binding option, - doms : ((((string * string option) list * binding) * mixfix) * + (doms : ((((string * string option) list * binding) * mixfix) * ((binding * (bool * binding option * string) list) * mixfix) list) list ) = let - val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; val specs : ((string * string option) list * binding * mixfix * (binding * (bool * binding option * string) list * mixfix) list) list = map (fn (((vs, t), mx), cons) => (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; - val comp_dbind = - case opt_name of NONE => Binding.name (space_implode "_" names) - | SOME s => s; in - if definitional - then add_new_domain_cmd comp_dbind specs - else add_domain_cmd comp_dbind specs + if definitional + then add_new_domain_cmd specs + else add_domain_cmd specs end; val _ = diff -r 4d1a8fa8cdfd -r 429cd74f795f src/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOLCF/Tools/Domain/domain_induction.ML Sat Oct 23 11:04:26 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_induction.ML Sat Oct 23 19:56:33 2010 -0700 @@ -8,7 +8,7 @@ signature DOMAIN_INDUCTION = sig val comp_theorems : - binding -> binding list -> + binding list -> Domain_Take_Proofs.take_induct_info -> Domain_Constructors.constr_info list -> theory -> thm list * theory @@ -367,13 +367,14 @@ (******************************************************************************) fun comp_theorems - (comp_dbind : binding) (dbinds : binding list) (take_info : Domain_Take_Proofs.take_induct_info) (constr_infos : Domain_Constructors.constr_info list) (thy : theory) = let -val comp_dname = Binding.name_of comp_dbind; + +val comp_dname = space_implode "_" (map Binding.name_of dbinds); +val comp_dbind = Binding.name comp_dname; (* Test for emptiness *) (* FIXME: reimplement emptiness test