clarified bindings;

--- a/src/HOL/Tools/Function/function.ML	Sun Apr 17 20:54:17 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Apr 17 22:10:09 2016 +0200
@@ -51,12 +51,10 @@
   @{attributes [nitpick_psimp]}
 
 fun note_qualified suffix attrs (fname, thms) =
-  Local_Theory.note ((Binding.qualify_name true fname suffix,
-    map (Attrib.internal o K) attrs), thms)
+  Local_Theory.note ((derived_name fname suffix, map (Attrib.internal o K) attrs), thms)
   #> apfst snd
 
-fun add_simps fnames post sort extra_qualify label mod_binding moreatts
-  simps lthy =
+fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
   let
     val spec = post simps
       |> map (apfst (apsnd (fn ats => moreatts @ ats)))
@@ -69,7 +67,7 @@
     val simps_by_f = sort saved_simps
 
     fun note fname simps =
-      Local_Theory.note ((mod_binding (Binding.qualify_name true fname label), []), simps) #> snd
+      Local_Theory.note ((mod_binding (derived_name fname label), []), simps) #> snd
   in (saved_simps, fold2 note fnames simps_by_f lthy) end
 
 fun prepare_function do_print prep fixspec eqns config lthy =
@@ -103,7 +101,6 @@
 
         val pelims = Function_Elims.mk_partial_elim_rules lthy result
 
-        val qualify = Binding.qualify_name true defname
         val concealed_partial = if partials then I else Binding.concealed
 
         val addsmps = add_simps fnames post sort_cont
@@ -112,19 +109,20 @@
           lthy
           |> addsmps (concealed_partial o Binding.qualify false "partial")
                "psimps" concealed_partial psimp_attribs psimps
-          ||>> Local_Theory.notes [((concealed_partial (qualify "pinduct"), []),
+          ||>> Local_Theory.notes [((concealed_partial (derived_name defname "pinduct"), []),
                 simple_pinducts |> map (fn th => ([th],
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
                   Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
                   Attrib.internal (K (Induct.induct_pred ""))])))]
           ||>> (apfst snd o
-            Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination]))
+            Local_Theory.note
+              ((Binding.concealed (derived_name defname "termination"), []), [termination]))
           ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames])
             (fnames ~~ map single cases) (* TODO: case names *)
           ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1])
             (fnames ~~ pelims)
           ||> (case domintros of NONE => I | SOME thms =>
-                Local_Theory.note ((qualify "domintros", []), thms) #> snd)
+                Local_Theory.note ((derived_name defname "domintros", []), thms) #> snd)
 
         val info =
           { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
@@ -204,8 +202,7 @@
         lthy
         |> add_simps I "simps" I simp_attribs tsimps
         ||>> Local_Theory.note
-           ((Binding.qualify_name true defname "induct",
-             [Attrib.internal (K (Rule_Cases.case_names case_names))]),
+           ((derived_name defname "induct", [Attrib.internal (K (Rule_Cases.case_names case_names))]),
             tinduct)
         ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1])
           (fnames ~~ telims)

--- a/src/HOL/Tools/Function/function_common.ML	Sun Apr 17 20:54:17 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Apr 17 22:10:09 2016 +0200
@@ -58,10 +58,6 @@
   val profile : bool Unsynchronized.ref
   val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
   val mk_acc : typ -> term -> term
-  val function_name : string -> string
-  val graph_name : string -> string
-  val rel_name : string -> string
-  val dom_name : string -> string
   val split_def : Proof.context -> (string -> 'a) -> term ->
     string * (string * typ) list * term list * term list * term
   val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit
@@ -125,11 +121,6 @@
 fun mk_acc domT R =
   Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R
 
-val function_name = suffix "C"
-val graph_name = suffix "_graph"
-val rel_name = suffix "_rel"
-val dom_name = suffix "_dom"
-
 
 (* analyzing function equations *)
 

--- a/src/HOL/Tools/Function/function_core.ML	Sun Apr 17 20:54:17 2016 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Apr 17 22:10:09 2016 +0200
@@ -492,14 +492,14 @@
   let
     val f_def_binding =
       Thm.make_def_binding (Config.get lthy function_internals)
-        (Binding.map_name (suffix "_sumC") defname)
+        (derived_name_suffix defname "_sumC")
     val f_def =
       Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT)
         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
       |> Syntax.check_term lthy
   in
-    Local_Theory.define
-      ((Binding.name (function_name fname), mixfix), ((f_def_binding, []), f_def)) lthy
+    lthy |> Local_Theory.define
+      ((Binding.name (fname ^ "C") (* FIXME proper binding *), mixfix), ((f_def_binding, []), f_def))
   end
 
 fun define_recursion_relation (R_binding, R_type) qglrs clauses RCss lthy =
@@ -851,7 +851,7 @@
     val ((G, GIntro_thms, G_elim, G_induct), lthy) =
       PROFILE "def_graph"
         (define_graph
-          (Binding.map_name graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy
+          (derived_name_suffix defname "_graph", domT --> ranT --> boolT) fvar clauses RCss) lthy
 
     val ((f, (_, f_defthm)), lthy) =
       PROFILE "def_fun" (define_function defname (fname, mixfix) domT ranT G default) lthy
@@ -861,13 +861,13 @@
 
     val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel"
-        (define_recursion_relation (Binding.map_name rel_name defname, domT --> domT --> boolT)
+        (define_recursion_relation (derived_name_suffix defname "_rel", domT --> domT --> boolT)
           abstract_qglrs clauses RCss) lthy
 
     val dom = mk_acc domT R
     val (_, lthy) =
       Local_Theory.abbrev Syntax.mode_default
-        (((Binding.map_name dom_name defname), NoSyn), dom) lthy
+        ((name_suffix defname "_dom", NoSyn), dom) lthy
 
     val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses

--- a/src/HOL/Tools/Function/function_lib.ML	Sun Apr 17 20:54:17 2016 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Sun Apr 17 22:10:09 2016 +0200
@@ -9,6 +9,10 @@
 sig
   val function_internals: bool Config.T
 
+  val derived_name: binding -> string -> binding
+  val name_suffix: binding -> string -> binding
+  val derived_name_suffix: binding -> string -> binding
+
   val plural: string -> string -> 'a list -> string
 
   val dest_all_all: term -> term list * term
@@ -34,6 +38,12 @@
 
 val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false)
 
+fun derived_name binding name =
+  Binding.reset_pos (Binding.qualify_name true binding name)
+
+fun name_suffix binding sffx = Binding.map_name (suffix sffx) binding
+fun derived_name_suffix binding sffx = Binding.reset_pos (name_suffix binding sffx)
+
 
 (* "The variable" ^ plural " is" "s are" vs *)
 fun plural sg pl [x] = sg

--- a/src/HOL/Tools/Function/partial_function.ML	Sun Apr 17 20:54:17 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Sun Apr 17 22:10:09 2016 +0200
@@ -17,6 +17,9 @@
 structure Partial_Function: PARTIAL_FUNCTION =
 struct
 
+open Function_Lib
+
+
 (*** Context Data ***)
 
 datatype setup_data = Setup_Data of
@@ -230,8 +233,7 @@
     val f_bname = Binding.name_of f_binding;
 
     fun note_qualified (name, thms) =
-      Local_Theory.note ((Binding.qualify_name true (Binding.reset_pos f_binding) name, []), thms)
-        #> snd
+      Local_Theory.note ((derived_name f_binding name, []), thms) #> snd
 
     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
     val (head, args) = strip_comb lhs;