src/HOL/Tools/Function/function_core.ML

 signature FUNCTION_CORE =
 sig
   val trace: bool Unsynchronized.ref
   val prepare_function : Function_Common.function_config
     -> binding (* defname *)
-    -> ((bstring * typ) * mixfix) list (* defined symbol *)
-    -> ((bstring * typ) list * term list * term * term) list (* specification *)
+    -> ((binding * typ) * mixfix) list (* defined symbol *)
+    -> ((string * typ) list * term list * term * term) list (* specification *)
     -> local_theory
     -> (term   (* f *)
         * thm  (* goalstate *)
         * (Proof.context -> thm -> Function_Common.function_result) (* continuation *)
        ) * local_theory

       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
     lthy |> Local_Theory.define
-      ((Binding.name (fname ^ "C") (* FIXME proper binding *), mixfix), ((f_def_binding, []), f_def))
+      ((Binding.map_name (suffix "C") fname, mixfix), ((f_def_binding, []), f_def))
   end
 
 fun define_recursion_relation (R_binding, R_type) qglrs clauses RCss lthy =
   let
     val R = Free (Binding.name_of R_binding, R_type)

 
 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
   let
     val FunctionConfig {domintros, default=default_opt, ...} = config
 
-    val default_str = the_default "%x. HOL.undefined" default_opt
-    val fvar = Free (fname, fT)
+    val default_str = the_default "%x. HOL.undefined" (* FIXME proper term!? *) default_opt
+    val fvar = (Binding.name_of fname, fT)
     val domT = domain_type fT
     val ranT = range_type fT
 
     val default = Syntax.parse_term lthy default_str
       |> Type.constraint fT |> Syntax.check_term lthy
 
-    val (globals, ctxt') = fix_globals domT ranT fvar lthy
+    val (globals, ctxt') = fix_globals domT ranT (Free fvar) lthy
 
     val Globals { x, h, ... } = globals
 
     val clauses = map (mk_clause_context x ctxt') abstract_qglrs
 
     val n = length abstract_qglrs
 
     fun build_tree (ClauseContext { ctxt, rhs, ...}) =
-       Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs
+       Function_Context_Tree.mk_tree fvar h ctxt rhs
 
     val trees = map build_tree clauses
     val RCss = map find_calls trees
 
     val ((G, GIntro_thms, G_elim, G_induct), lthy) =
       PROFILE "def_graph"
         (define_graph
-          (derived_name_suffix defname "_graph", domT --> ranT --> boolT) fvar clauses RCss) lthy
+          (derived_name_suffix defname "_graph", domT --> ranT --> boolT) (Free fvar) clauses RCss)
+        lthy
 
     val ((f, (_, f_defthm)), 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 RCss = map (map (inst_RC lthy (Free fvar) f)) RCss
+    val trees = map (Function_Context_Tree.inst_tree lthy (Free fvar) f) trees
 
     val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel"
         (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
-        ((name_suffix defname "_dom", NoSyn), dom) lthy
+        ((derived_name_suffix defname "_dom", NoSyn), dom) lthy
 
     val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses
 
     val xclauses = PROFILE "xclauses"

 
     val complete =
       mk_completeness globals clauses abstract_qglrs |> Thm.cterm_of lthy |> Thm.assume
 
     val compat =
-      mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
+      mk_compat_proof_obligations domT ranT (Free fvar) f abstract_qglrs
       |> map (Thm.cterm_of lthy #> Thm.assume)
 
     val compat_store = store_compat_thms n compat
 
     val (goalstate, values) = PROFILE "prove_stuff"

       end
   in
     ((f, goalstate, mk_partial_rules), lthy)
   end
 
-
 end