# HG changeset patch
# User wenzelm
# Date 1460919257 -7200
# Node ID f507e6fe1d77cad334a62208f093de10f11998ef
# Parent  bf5fcc65586b2067651933f74dc13303365d7df2
prefer binding over base name;

diff -r bf5fcc65586b -r f507e6fe1d77 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sun Apr 17 20:54:17 2016 +0200
@@ -1822,13 +1822,13 @@
     (plugins, friend, transfer)
   end;
 
-fun add_function name parsed_eq lthy =
+fun add_function binding parsed_eq lthy =
   let
     fun pat_completeness_auto ctxt =
       Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt;
 
     val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
-      Function.add_function [(Binding.concealed (Binding.name name), NONE, NoSyn)]
+      Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
         [(apfst Binding.concealed Attrib.empty_binding, parsed_eq)]
         Function_Common.default_config pat_completeness_auto lthy;
   in
@@ -1847,7 +1847,7 @@
           mk_Trueprop_eq (betapply (inner_fp_free, arg), betapply (explored_rhs, arg));
 
         val ((inner_fp_name, (pelim, pinduct, psimp)), lthy') =
-          add_function inner_fp_name0 inner_fp_eq lthy;
+          add_function (Binding.name inner_fp_name0) inner_fp_eq lthy;
 
         fun mk_triple elim induct simp = ([elim], [induct], [simp]);
 
@@ -1870,7 +1870,7 @@
           else
             prepare_termin ();
 
-        val inner_fp_const = (inner_fp_name, fastype_of explored_rhs)
+        val inner_fp_const = (Binding.name_of inner_fp_name, fastype_of explored_rhs)
           |>> Proof_Context.read_const {proper = true, strict = false} lthy'
           |> (fn (Const (s, _), T) => Const (s, T));
       in
diff -r bf5fcc65586b -r f507e6fe1d77 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Apr 17 20:54:17 2016 +0200
@@ -51,7 +51,7 @@
   @{attributes [nitpick_psimp]}
 
 fun note_qualified suffix attrs (fname, thms) =
-  Local_Theory.note ((Binding.qualify true fname (Binding.name suffix),
+  Local_Theory.note ((Binding.qualify_name true fname suffix,
     map (Attrib.internal o K) attrs), thms)
   #> apfst snd
 
@@ -68,13 +68,9 @@
     val saved_simps = maps snd saved_spec_simps
     val simps_by_f = sort saved_simps
 
-    fun add_for_f fname simps =
-      Local_Theory.note
-        ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
-      #> snd
-  in
-    (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
-  end
+    fun note fname simps =
+      Local_Theory.note ((mod_binding (Binding.qualify_name true 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 =
   let
@@ -83,8 +79,12 @@
     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
 
-    val fnames = map (fst o fst) fixes
-    val defname = space_implode "_" fnames
+    val fnames = map (fst o fst) fixes0
+    val f_base_names = map (fst o fst) fixes
+    val defname =
+      (case fixes0 of
+        [((b, _), _)] => b
+      | _ => Binding.name (space_implode "_" f_base_names))
 
     val FunctionConfig {partials, default, ...} = config
     val _ =
@@ -103,8 +103,7 @@
 
         val pelims = Function_Elims.mk_partial_elim_rules lthy result
 
-        fun qualify n = Binding.name n
-          |> Binding.qualify true defname
+        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
@@ -118,13 +117,17 @@
                  [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]))
-          ||>> 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)
+          ||>> (apfst snd o
+            Local_Theory.note ((Binding.concealed (qualify "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 ((qualify "domintros", []), thms) #> snd)
 
-        val info = { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
+        val info =
+          { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
           pelims=pelims',elims=NONE}
@@ -135,7 +138,7 @@
       in
         (info,
          lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
-          (add_function_data o transform_function_data info))
+          (fn phi => add_function_data (transform_function_data phi info)))
       end
   in
     ((goal_state, afterqed), lthy')
@@ -197,18 +200,15 @@
         val tsimps = map remove_domain_condition psimps
         val tinduct = map remove_domain_condition pinducts
         val telims = map (map remove_domain_condition) pelims
-
-        fun qualify n = Binding.name n
-          |> Binding.qualify true defname
-
       in
         lthy
         |> add_simps I "simps" I simp_attribs tsimps
         ||>> Local_Theory.note
-           ((qualify "induct",
+           ((Binding.qualify_name true 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)
+        ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1])
+          (fnames ~~ telims)
         |-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
           let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
             case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
@@ -217,7 +217,7 @@
             (info',
              lthy
              |> Local_Theory.declaration {syntax = false, pervasive = false}
-               (add_function_data o transform_function_data info')
+               (fn phi => add_function_data (transform_function_data phi info'))
              |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
           end)
       end
@@ -291,5 +291,4 @@
     "prove termination of a recursive function"
     (Scan.option Parse.term >> termination_cmd)
 
-
 end
diff -r bf5fcc65586b -r f507e6fe1d77 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Apr 17 20:54:17 2016 +0200
@@ -8,11 +8,11 @@
 sig
   type info =
    {is_partial : bool,
-    defname : string,
+    defname : binding,
       (*contains no logical entities: invariant under morphisms:*)
     add_simps : (binding -> binding) -> string -> (binding -> binding) ->
       Token.src list -> thm list -> local_theory -> thm list * local_theory,
-    fnames : string list,
+    fnames : binding list,
     case_names : string list,
     fs : term list,
     R : term,
@@ -32,11 +32,11 @@
 
 type info =
  {is_partial : bool,
-  defname : string,
+  defname : binding,
     (*contains no logical entities: invariant under morphisms:*)
   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
     Token.src list -> thm list -> local_theory -> thm list * local_theory,
-  fnames : string list,
+  fnames : binding list,
   case_names : string list,
   fs : term list,
   R : term,
@@ -98,7 +98,7 @@
     pelims : thm list list,
     termination : thm,
     domintros : thm list option}
-  val transform_function_data : info -> morphism -> info
+  val transform_function_data : morphism -> info -> info
   val import_function_data : term -> Proof.context -> info option
   val import_last_function : Proof.context -> info option
   val default_config : function_config
@@ -300,19 +300,18 @@
   termination : thm,
   domintros : thm list option}
 
-fun transform_function_data ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
-  simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) phi =
+fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
+  simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) =
     let
       val term = Morphism.term phi
       val thm = Morphism.thm phi
       val fact = Morphism.fact phi
-      val name = Binding.name_of o Morphism.binding phi o Binding.name
     in
       { add_simps = add_simps, case_names = case_names, fnames = fnames,
         fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
         pinducts = fact pinducts, simps = Option.map fact simps,
         inducts = Option.map fact inducts, termination = thm termination,
-        defname = name defname, is_partial=is_partial, cases = fact cases,
+        defname = Morphism.binding phi defname, is_partial=is_partial, cases = fact cases,
         elims = Option.map (map fact) elims, pelims = map fact pelims }
     end
 
@@ -333,7 +332,7 @@
     val inst_morph = lift_morphism ctxt o Thm.instantiate
 
     fun match (trm, data) =
-      SOME (transform_function_data data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))))
+      SOME (transform_function_data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))) data)
         handle Pattern.MATCH => NONE
   in
     get_first match (Item_Net.retrieve (get_functions ctxt) t)
diff -r bf5fcc65586b -r f507e6fe1d77 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Apr 17 20:54:17 2016 +0200
@@ -8,7 +8,7 @@
 sig
   val trace: bool Unsynchronized.ref
   val prepare_function : Function_Common.function_config
-    -> string (* defname *)
+    -> binding (* defname *)
     -> ((bstring * typ) * mixfix) list (* defined symbol *)
     -> ((bstring * typ) list * term list * term * term) list (* specification *)
     -> local_theory
@@ -469,9 +469,9 @@
     ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   end
 
-fun define_graph (G_name, G_type) fvar clauses RCss lthy =
+fun define_graph (G_binding, G_type) fvar clauses RCss lthy =
   let
-    val G = Free (G_name, G_type)
+    val G = Free (Binding.name_of G_binding, G_type)
     fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
       let
         fun mk_h_assm (rcfix, rcassm, rcarg) =
@@ -486,28 +486,27 @@
       end
 
     val G_intros = map2 mk_GIntro clauses RCss
-  in
-    inductive_def ((Binding.name G_name, G_type), NoSyn) G_intros lthy
-  end
+  in inductive_def ((G_binding, G_type), NoSyn) G_intros lthy end
 
-fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
+fun define_function defname (fname, mixfix) domT ranT G default lthy =
   let
+    val f_def_binding =
+      Thm.make_def_binding (Config.get lthy function_internals)
+        (Binding.map_name (suffix "_sumC") defname)
     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
-    val def_binding =
-      if Config.get lthy function_internals then (Binding.name fdefname, [])
-      else Attrib.empty_binding
   in
     Local_Theory.define
-      ((Binding.name (function_name fname), mixfix), (def_binding, f_def)) lthy
+      ((Binding.name (function_name fname), mixfix), ((f_def_binding, []), f_def)) lthy
   end
 
-fun define_recursion_relation (R_name, R_type) qglrs clauses RCss lthy =
+fun define_recursion_relation (R_binding, R_type) qglrs clauses RCss lthy =
   let
+    val R = Free (Binding.name_of R_binding, R_type)
     fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
-      HOLogic.mk_Trueprop (Free (R_name, R_type) $ rcarg $ lhs)
+      HOLogic.mk_Trueprop (R $ rcarg $ lhs)
       |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
       |> fold_rev (curry Logic.mk_implies) gs
       |> fold_rev (Logic.all o Free) rcfix
@@ -517,7 +516,7 @@
     val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
     val ((R, RIntro_thms, R_elim, _), lthy) =
-      inductive_def ((Binding.name R_name, R_type), NoSyn) (flat R_intross) lthy
+      inductive_def ((R_binding, R_type), NoSyn) (flat R_intross) lthy
   in
     ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
   end
@@ -851,22 +850,24 @@
 
     val ((G, GIntro_thms, G_elim, G_induct), lthy) =
       PROFILE "def_graph"
-        (define_graph (graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy
+        (define_graph
+          (Binding.map_name graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy
 
     val ((f, (_, f_defthm)), lthy) =
-      PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
+      PROFILE "def_fun" (define_function defname (fname, mixfix) domT ranT G default) lthy
 
     val RCss = map (map (inst_RC lthy fvar f)) RCss
     val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
 
     val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel"
-        (define_recursion_relation (rel_name defname, domT --> domT --> boolT)
+        (define_recursion_relation (Binding.map_name rel_name defname, domT --> domT --> boolT)
           abstract_qglrs clauses RCss) lthy
 
     val dom = mk_acc domT R
     val (_, lthy) =
-      Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), dom) lthy
+      Local_Theory.abbrev Syntax.mode_default
+        (((Binding.map_name dom_name defname), NoSyn), dom) lthy
 
     val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses
diff -r bf5fcc65586b -r f507e6fe1d77 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun Apr 17 20:54:17 2016 +0200
@@ -7,7 +7,7 @@
 signature FUNCTION_MUTUAL =
 sig
   val prepare_function_mutual : Function_Common.function_config
-    -> string (* defname *)
+    -> binding (* defname *)
     -> ((string * typ) * mixfix) list
     -> term list
     -> local_theory
@@ -90,7 +90,8 @@
 
     val fsum_type = ST --> RST
 
-    val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
+    val ([fsum_var_name], _) =
+      Variable.add_fixes_binding [Binding.map_name (suffix "_sum") defname] ctxt
     val fsum_var = (fsum_var_name, fsum_type)
 
     fun define (fvar as (n, _)) caTs resultT i =