--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 13 20:04:24 2012 +0100
@@ -83,7 +83,7 @@
fun mk_const (b, T, _) = Const (Sign.full_name thy b, T)
val consts = map mk_const decls
fun mk_def c (b, t, _) =
- (Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
+ (Thm.def_binding b, Logic.mk_equals (c, t))
val defs = map2 mk_def consts specs
val (def_thms, thy) =
Global_Theory.add_defs false (map Thm.no_attributes defs) thy
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 13 20:04:24 2012 +0100
@@ -151,7 +151,7 @@
(* register constant definitions *)
val (fixdef_thms, thy) =
(Global_Theory.add_defs false o map Thm.no_attributes)
- (map (Binding.suffix_name "_def") binds ~~ eqns) thy
+ (map Thm.def_binding binds ~~ eqns) thy
(* prove applied version of definitions *)
fun prove_proj (lhs, rhs) =
@@ -232,7 +232,7 @@
val typ = Term.fastype_of rhs
val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy
val eqn = Logic.mk_equals (const, rhs)
- val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn)
+ val def = Thm.no_attributes (Thm.def_binding bind, eqn)
val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy
in
((const, def_thm), thy)
--- a/src/HOL/HOLCF/Tools/cpodef.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Tue Mar 13 20:04:24 2012 +0100
@@ -195,7 +195,7 @@
val ((_, (_, below_ldef)), lthy) = thy
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
|> Specification.definition (NONE,
- ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn))
+ ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn))
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
val thy = lthy
--- a/src/HOL/HOLCF/Tools/domaindef.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Tue Mar 13 20:04:24 2012 +0100
@@ -134,7 +134,7 @@
Abs ("t", Term.itselfT newT,
mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT)))
- val name_def = Binding.suffix_name "_def" name
+ val name_def = Thm.def_binding name
val emb_bind = (Binding.prefix_name "emb_" name_def, [])
val prj_bind = (Binding.prefix_name "prj_" name_def, [])
val defl_bind = (Binding.prefix_name "defl_" name_def, [])
--- a/src/HOL/HOLCF/Tools/fixrec.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Tue Mar 13 20:04:24 2012 +0100
@@ -141,7 +141,7 @@
fun one_def (Free(n,_)) r =
let val b = Long_Name.base_name n
- in ((Binding.name (b^"_def"), []), r) end
+ in ((Binding.name (Thm.def_name b), []), r) end
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
fun defs [] _ = []
| defs (l::[]) r = [one_def l r]
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Mar 13 20:04:24 2012 +0100
@@ -394,7 +394,7 @@
fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T);
val consts = map mk_const decls;
fun mk_def c (b, t, mx) =
- (Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
+ (Thm.def_binding b, Logic.mk_equals (c, t));
val defs = map2 mk_def consts specs;
val (def_thms, thy) =
Global_Theory.add_defs false (map Thm.no_attributes defs) thy;
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue Mar 13 20:04:24 2012 +0100
@@ -235,7 +235,7 @@
val lhs = list_comb (Const (cname, constrT), l_args);
val rhs = mk_univ_inj r_args n i;
val def = Logic.mk_equals (lhs, Const (Abs_name, Univ_elT --> T) $ rhs);
- val def_name = Long_Name.base_name cname ^ "_def";
+ val def_name = Thm.def_name (Long_Name.base_name cname);
val eqn =
HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs));
val ([def_thm], thy') =
@@ -345,7 +345,7 @@
val fTs = map fastype_of fs;
val defs =
map (fn (rec_name, (T, iso_name)) =>
- (Binding.name (Long_Name.base_name iso_name ^ "_def"),
+ (Binding.name (Thm.def_name (Long_Name.base_name iso_name)),
Logic.mk_equals (Const (iso_name, T --> Univ_elT),
list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
val (def_thms, thy') =
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Tue Mar 13 20:04:24 2012 +0100
@@ -233,7 +233,7 @@
|> (Global_Theory.add_defs false o map Thm.no_attributes)
(map
(fn ((((name, comb), set), T), T') =>
- (Binding.name (Long_Name.base_name name ^ "_def"),
+ (Binding.name (Thm.def_name (Long_Name.base_name name)),
Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
(Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
(set $ Free ("x", T) $ Free ("y", T')))))))
@@ -314,7 +314,7 @@
val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
val def =
- (Binding.name (Long_Name.base_name name ^ "_def"),
+ (Binding.name (Thm.def_name (Long_Name.base_name name)),
Logic.mk_equals (Const (name, caseT),
fold_rev lambda fns1
(list_comb (reccomb,
--- a/src/HOL/Tools/Function/mutual.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Function/mutual.ML Tue Mar 13 20:04:24 2012 +0100
@@ -134,7 +134,7 @@
val ((f, (_, f_defthm)), lthy') =
Local_Theory.define
((Binding.name fname, mixfix),
- ((Binding.conceal (Binding.name (fname ^ "_def")), []),
+ ((Binding.conceal (Binding.name (Thm.def_name fname)), []),
Term.subst_bound (fsum, f_def))) lthy
in
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Mar 13 20:04:24 2012 +0100
@@ -1152,7 +1152,7 @@
val def = Logic.mk_equals (lhs, predterm)
val ([definition], thy') = thy |>
Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
- Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
+ Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
val ctxt' = Proof_Context.init_global thy'
val rules as ((intro, elim), _) =
create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Mar 13 20:04:24 2012 +0100
@@ -87,7 +87,7 @@
val def = Logic.mk_equals (lhs, atom)
val ([definition], thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
in
(lhs, ((full_constname, [definition]) :: defs, thy'))
end
@@ -249,7 +249,7 @@
val def = Logic.mk_equals (lhs, abs_arg')
val ([definition], thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
in
(list_comb (Logic.varify_global const, vars),
((full_constname, [definition])::new_defs, thy'))
--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Mar 13 20:04:24 2012 +0100
@@ -45,7 +45,7 @@
quote str ^ " differs from declaration " ^ name ^ pos)
end
-fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
+fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy =
let
val (vars, ctxt) = prep_vars (the_list raw_var) lthy
val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
@@ -69,7 +69,8 @@
val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Local_Defs.abs_def prop'
- val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
+ val ((trm, (_ , thm)), lthy') =
+ Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
(* data storage *)
val qconst_data = {qconst = trm, rconst = rhs, def = thm}
--- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Mar 13 20:04:24 2012 +0100
@@ -109,9 +109,9 @@
| SOME morphs => morphs)
val ((abs_t, (_, abs_def)), lthy2) = lthy1
- |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
+ |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
val ((rep_t, (_, rep_def)), lthy3) = lthy2
- |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
+ |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
(* quot_type theorem *)
val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
--- a/src/HOL/Tools/TFL/tfl.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Mar 13 20:04:24 2012 +0100
@@ -371,7 +371,7 @@
val (wfrec,_) = USyntax.strip_comb rhs
in
fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
- let val def_name = Long_Name.base_name fid ^ "_def"
+ let val def_name = Thm.def_name (Long_Name.base_name fid)
val wfrec_R_M = map_types poly_tvars
(wfrec $ map_types poly_tvars R)
$ functional
@@ -537,7 +537,7 @@
val ([def0], theory) =
thy
|> Global_Theory.add_defs false
- [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
+ [Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
val def = Thm.unvarify_global def0;
val dummy =
if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
--- a/src/HOL/Tools/inductive_set.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/inductive_set.ML Tue Mar 13 20:04:24 2012 +0100
@@ -498,7 +498,7 @@
val (defs, lthy2) = lthy1
|> Local_Theory.conceal (* FIXME ?? *)
|> fold_map Local_Theory.define
- (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
+ (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
fold_rev lambda params (HOLogic.Collect_const U $
HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds))
--- a/src/Pure/Proof/extraction.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/Pure/Proof/extraction.ML Tue Mar 13 20:04:24 2012 +0100
@@ -728,7 +728,7 @@
(chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
(chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
(chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
- PAxm (cname ^ "_def", eqn,
+ PAxm (Thm.def_name cname, eqn,
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Reconstruct.prop_of corr_prf';
val corr_prf'' =
@@ -792,7 +792,8 @@
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
|> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
- |> Global_Theory.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
+ |> Global_Theory.add_defs false
+ [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
thy'
--- a/src/Tools/interpretation_with_defs.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/Tools/interpretation_with_defs.ML Tue Mar 13 20:04:24 2012 +0100
@@ -45,8 +45,8 @@
val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
|> Syntax.check_terms defs_ctxt;
- val defs = map2 (fn (binding_thm, (binding_syn, _)) => fn rhs =>
- (binding_syn, (binding_thm, rhs))) raw_defs rhss;
+ val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
+ ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
val (def_eqns, theory') = theory
|> Named_Target.theory_init
--- a/src/Tools/misc_legacy.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/Tools/misc_legacy.ML Tue Mar 13 20:04:24 2012 +0100
@@ -96,7 +96,7 @@
fun mk_defpair (lhs, rhs) =
(case Term.head_of lhs of
Const (name, _) =>
- (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
+ (Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs))
| _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));