--- 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
--- 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
--- 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
--- 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 ***************************)
--- 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 ***************************)
--- 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);
--- 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 *)
--- 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),
--- 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
--- 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}, _) =>
--- 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]}
--- 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);
--- 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);
--- 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;
--- 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