# HG changeset patch
# User wenzelm
# Date 1331665464 -3600
# Node ID 3c73a121a387a346798a5756b4dad958be853b31
# Parent  3553cb65c66c67d63d9a61dc80e4713821a32595
more explicit indication of def names;

diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- 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
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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)
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/HOLCF/Tools/cpodef.ML
--- 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
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/HOLCF/Tools/domaindef.ML
--- 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, [])
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/HOLCF/Tools/fixrec.ML
--- 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]
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/HOLCF/ex/Pattern_Match.thy
--- 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;
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/Datatype/datatype.ML
--- 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') =
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/Datatype/rep_datatype.ML
--- 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,
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/Function/mutual.ML
--- 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,
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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))
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- 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'))
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/Quotient/quotient_def.ML
--- 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}
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/Quotient/quotient_type.ML
--- 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
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/TFL/tfl.ML
--- 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)
diff -r 3553cb65c66c -r 3c73a121a387 src/HOL/Tools/inductive_set.ML
--- 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))
diff -r 3553cb65c66c -r 3c73a121a387 src/Pure/Proof/extraction.ML
--- 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'
diff -r 3553cb65c66c -r 3c73a121a387 src/Tools/interpretation_with_defs.ML
--- 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
diff -r 3553cb65c66c -r 3c73a121a387 src/Tools/misc_legacy.ML
--- 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]));