# HG changeset patch # User wenzelm # Date 1460916662 -7200 # Node ID bf5fcc65586b2067651933f74dc13303365d7df2 # Parent 56cf1249ee203e1984d86f76740df51418dcd801 clarified signature; diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sun Apr 17 20:11:02 2016 +0200 @@ -51,8 +51,8 @@ val rep_iso_eqn = Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))) - val abs_iso_bind = Binding.qualified true "abs_iso" dbind - val rep_iso_bind = Binding.qualified true "rep_iso" dbind + val abs_iso_bind = Binding.qualify_name true dbind "abs_iso" + val rep_iso_bind = Binding.qualify_name true dbind "rep_iso" val (abs_iso_thm, thy) = Specification.axiom ((abs_iso_bind, []), abs_iso_eqn) thy val (rep_iso_thm, thy) = Specification.axiom ((rep_iso_bind, []), rep_iso_eqn) thy @@ -81,7 +81,7 @@ val lub_take_eqn = mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)) - val lub_take_bind = Binding.qualified true "lub_take" dbind + val lub_take_bind = Binding.qualify_name true dbind "lub_take" val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy in diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Apr 17 20:11:02 2016 +0200 @@ -929,7 +929,7 @@ (* bind theorem names in global theory *) val (_, thy) = let - fun qualified name = Binding.qualified true name dbind + fun qualified name = Binding.qualify_name true dbind name val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec val dname = fst (dest_Type lhsT) val simp = Simplifier.simp_add diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Apr 17 20:11:02 2016 +0200 @@ -78,7 +78,7 @@ val take_apps = map prove_take_app con_specs in yield_singleton Global_Theory.add_thmss - ((Binding.qualified true "take_rews" dbind, take_apps), + ((Binding.qualify_name true dbind "take_rews", take_apps), [Simplifier.simp_add]) thy end in @@ -235,8 +235,8 @@ in thy |> snd o Global_Theory.add_thms [ - ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), - ((Binding.qualified true "induct" comp_dbind, ind ), [])] + ((Binding.qualify_name true comp_dbind "finite_induct", finite_ind), []), + ((Binding.qualify_name true comp_dbind "induct", ind), [])] |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) end (* prove_induction *) @@ -301,7 +301,7 @@ in val (bisim_def_thm, thy) = thy |> yield_singleton (Global_Theory.add_defs false) - ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []) + ((Binding.qualify_name true comp_dbind "bisim_def", bisim_eqn), []) end (* local *) (* prove coinduction lemma *) @@ -357,7 +357,7 @@ Goal.prove_global thy [] [assm1, assm2] goal tacf end val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms) - val coind_binds = map (Binding.qualified true "coinduct") dbinds + val coind_binds = map (fn b => Binding.qualify_name true b "coinduct") dbinds in thy |> snd o Global_Theory.add_thms diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Apr 17 20:11:02 2016 +0200 @@ -223,7 +223,7 @@ fun add_qualified_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms - ((Binding.qualified true name dbind, thm), []) + ((Binding.qualify_name true dbind name, thm), []) (******************************************************************************) (*************************** defining map functions ***************************) diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Apr 17 20:11:02 2016 +0200 @@ -187,15 +187,15 @@ fun add_qualified_def name (dbind, eqn) = yield_singleton (Global_Theory.add_defs false) - ((Binding.qualified true name dbind, eqn), []) + ((Binding.qualify_name true dbind name, eqn), []) fun add_qualified_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms - ((Binding.qualified true name dbind, thm), []) + ((Binding.qualify_name true dbind name, thm), []) fun add_qualified_simp_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms - ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]) + ((Binding.qualify_name true dbind name, thm), [Simplifier.simp_add]) (******************************************************************************) (************************** defining take functions ***************************) diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Sun Apr 17 20:11:02 2016 +0200 @@ -230,7 +230,7 @@ val f_bname = Binding.name_of f_binding; fun note_qualified (name, thms) = - Local_Theory.note ((Binding.qualified true name (Binding.reset_pos f_binding), []), thms) + Local_Theory.note ((Binding.qualify_name true (Binding.reset_pos f_binding) name, []), thms) #> snd val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn); diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Apr 17 20:11:02 2016 +0200 @@ -76,12 +76,8 @@ fun Quotient_map bnf ctxt = let val Quotient = prove_Quotient_map bnf ctxt - fun qualify defname suffix = Binding.qualified true suffix defname - val Quotient_thm_name = qualify (base_name_of_bnf bnf) "Quotient" - val notes = [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])] - in - notes - end + val Quotient_thm_name = Binding.qualify_name true (base_name_of_bnf bnf) "Quotient" + in [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])] end (* relator_eq_onp *) diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Sun Apr 17 20:11:02 2016 +0200 @@ -584,15 +584,13 @@ val abs_eq_thm = generate_abs_eq lthy def_thm rsp_thm quot_thm val opt_rep_eq_thm = generate_rep_eq lthy def_thm rsp_thm (rty_forced, qty) - fun qualify defname suffix = Binding.qualified true suffix defname - fun notes names = let val lhs_name = (#1 var) - val rsp_thmN = qualify lhs_name "rsp" - val abs_eq_thmN = qualify lhs_name "abs_eq" - val rep_eq_thmN = qualify lhs_name "rep_eq" - val transfer_ruleN = qualify lhs_name "transfer" + val rsp_thmN = Binding.qualify_name true lhs_name "rsp" + val abs_eq_thmN = Binding.qualify_name true lhs_name "abs_eq" + val rep_eq_thmN = Binding.qualify_name true lhs_name "rep_eq" + val transfer_ruleN = Binding.qualify_name true lhs_name "transfer" val notes = [(rsp_thmN, [], [rsp_thm]), (transfer_ruleN, @{attributes [transfer_rule]}, transfer_rules), diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Apr 17 20:11:02 2016 +0200 @@ -325,10 +325,12 @@ fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt THEN' (rtac ctxt @{thm id_transfer})); - val (rep_isom_lift_def, lthy) = lift_def ld_no_notes (Binding.qualified true "Rep_isom" uTname, NoSyn) + val (rep_isom_lift_def, lthy) = + lift_def ld_no_notes (Binding.qualify_name true uTname "Rep_isom", NoSyn) (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] lthy |> apfst (inst_of_lift_def lthy (qty_isom --> qty)); - val (abs_isom, lthy) = lift_def ld_no_notes (Binding.qualified true "Abs_isom" uTname, NoSyn) + val (abs_isom, lthy) = + lift_def ld_no_notes (Binding.qualify_name true uTname "Abs_isom", NoSyn) (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] lthy |> apfst (mk_lift_const_of_lift_def (qty --> qty_isom)); val rep_isom = lift_const_of_lift_def rep_isom_lift_def @@ -397,7 +399,7 @@ val sel_rhs = map (map mk_sel_rhs) sel_argss val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks val dis_qty = qty_isom --> HOLogic.boolT; - val dis_names = map (fn k => Binding.qualified true ("dis" ^ string_of_int k) uTname) ks; + val dis_names = map (fn k => Binding.qualify_name true uTname ("dis" ^ string_of_int k)) ks; val (diss, lthy) = @{fold_map 2} (fn b => fn rhs => fn lthy => lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy @@ -416,8 +418,10 @@ REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])) i val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps) - val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualified true - ("sel" ^ string_of_int k ^ string_of_int k') uTname) (1 upto length xs)) (ks ~~ ctr_Tss); + val sel_names = + map (fn (k, xs) => + map (fn k' => Binding.qualify_name true uTname ("sel" ^ string_of_int k ^ string_of_int k')) + (1 upto length xs)) (ks ~~ ctr_Tss); val (selss, lthy) = @{fold_map 2} (@{fold_map 2} (fn b => fn (qty_ret, wits, rhs) => fn lthy => lift_def_code_dt { code_dt = true, lift_config = ld_no_notes } (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun Apr 17 20:11:02 2016 +0200 @@ -155,7 +155,7 @@ |> mk_HOL_eq |> singleton (Variable.export lthy orig_lthy) val lthy = (#notes config ? (Local_Theory.note - ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) #> snd)) lthy + ((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> snd)) lthy in (thm, lthy) end @@ -238,8 +238,8 @@ fun lifting_bundle qty_full_name qinfo lthy = let - fun qualify suffix defname = Binding.qualified true suffix defname - val binding = qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting" + val binding = + Binding.qualify_name true (qty_full_name |> Long_Name.base_name |> Binding.name) "lifting" val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding val bundle_name = Name_Space.full_name (Name_Space.naming_of (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding @@ -526,23 +526,17 @@ val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty)))) val qty_full_name = (fst o dest_Type) qty val qty_name = (Binding.name o Long_Name.base_name) qty_full_name - fun qualify suffix = Binding.qualified true suffix qty_name + val qualify = Binding.qualify_name true qty_name val notes1 = case opt_reflp_thm of SOME reflp_thm => let val thms = - [("abs_induct", @{thms Quotient_total_abs_induct}, [induct_attr]), - ("abs_eq_iff", @{thms Quotient_total_abs_eq_iff}, [] )] - in - map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms - end + [("abs_induct", @{thms Quotient_total_abs_induct}, [induct_attr]), + ("abs_eq_iff", @{thms Quotient_total_abs_eq_iff}, [])] + in map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end | NONE => - let - val thms = - [("abs_induct", @{thms Quotient_abs_induct}, [induct_attr])] - in - map_thms qualify (fn thm => quot_thm RS thm) thms - end + let val thms = [("abs_induct", @{thms Quotient_abs_induct}, [induct_attr])] + in map_thms qualify (fn thm => quot_thm RS thm) thms end val dom_thm = get_Domainp_thm quot_thm fun setup_transfer_rules_nonpar notes = @@ -663,7 +657,7 @@ val (rty, qty) = quot_thm_rty_qty quot_thm val qty_full_name = (fst o dest_Type) qty val qty_name = (Binding.name o Long_Name.base_name) qty_full_name - fun qualify suffix = Binding.qualified true suffix qty_name + val qualify = Binding.qualify_name true qty_name val opt_reflp_thm = case typedef_set of Const (@{const_name top}, _) => diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Apr 17 20:11:02 2016 +0200 @@ -119,7 +119,6 @@ let val transfer_attr = @{attributes [transfer_rule]} val Tname = base_name_of_bnf bnf - fun qualify suffix = Binding.qualified true suffix Tname val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def} @@ -127,9 +126,8 @@ val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def} [snd (nth defs 2), snd (nth defs 3)] val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs - val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs in - notes + maps (fn (a, thm) => [((Binding.qualify_name true Tname a, []), [([thm], transfer_attr)])]) defs end (* relator_eq *) @@ -203,8 +201,7 @@ val pred_def = pred_set_of_bnf bnf val Domainp_rel = prove_Domainp_rel lthy bnf pred_def val rel_eq_onp = rel_eq_onp_of_bnf bnf - fun qualify defname suffix = Binding.qualified true suffix defname - val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel" + val Domainp_rel_thm_name = Binding.qualify_name true (base_name_of_bnf bnf) "Domainp_rel" val pred_data = Transfer.mk_pred_data pred_def rel_eq_onp [] val type_name = type_name_of_bnf bnf val relator_domain_attr = @{attributes [relator_domain]} diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/typedef.ML Sun Apr 17 20:11:02 2016 +0200 @@ -177,7 +177,7 @@ type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding}; fun prefix_binding prfx name = - Binding.reset_pos (Binding.qualified false (prfx ^ Binding.name_of name) name); + Binding.reset_pos (Binding.qualify_name false name (prfx ^ Binding.name_of name)); fun qualify_binding name = Binding.qualify false (Binding.name_of name); diff -r 56cf1249ee20 -r bf5fcc65586b src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/Pure/General/binding.ML Sun Apr 17 20:11:02 2016 +0200 @@ -26,7 +26,7 @@ val empty: binding val is_empty: binding -> bool val qualify: bool -> string -> binding -> binding - val qualified: bool -> string -> binding -> binding + val qualify_name: bool -> binding -> string -> binding val qualified_name: string -> binding val prefix_of: binding -> (string * bool) list val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding @@ -109,8 +109,8 @@ map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) => (restricted, concealed, prefix, (qual, mandatory) :: qualifier, name, pos)); -fun qualified mandatory name' = - map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) => +fun qualify_name mandatory binding name' = + binding |> map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) => let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)] in (restricted, concealed, prefix, qualifier', name', pos) end); diff -r 56cf1249ee20 -r bf5fcc65586b src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/Pure/General/name_space.ML Sun Apr 17 20:11:02 2016 +0200 @@ -381,7 +381,7 @@ fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]); fun qualified_path mandatory binding = map_path (fn path => - path @ Binding.path_of (Binding.qualified mandatory "" binding)); + path @ Binding.path_of (Binding.qualify_name mandatory binding "")); val global_naming = make_naming ([], NONE, false, NONE, "", []); val local_naming = global_naming |> add_path Long_Name.localN; diff -r 56cf1249ee20 -r bf5fcc65586b src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/Pure/Isar/proof.ML Sun Apr 17 20:11:02 2016 +0200 @@ -867,7 +867,7 @@ val (asms, state') = state |> map_context_result (fn ctxt => ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt internal (name, pos) xs)); val assumptions = - asms |> map (fn (a, ts) => ((Binding.qualified true a binding, []), map (rpair []) ts)); + asms |> map (fn (a, ts) => ((Binding.qualify_name true binding a, []), map (rpair []) ts)); in state' |> assume [] [] assumptions