# HG changeset patch
# User wenzelm
# Date 1460886809 -7200
# Node ID 1c52ea2954f5f1b11714a1c87b88287b5edf64f1
# Parent  7d5ac15ff88ff403476c296a26adc4bdf8d7709c
tuned;

diff -r 7d5ac15ff88f -r 1c52ea2954f5 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Apr 15 18:05:57 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Apr 17 11:53:29 2016 +0200
@@ -50,8 +50,6 @@
 val psimp_attribs =
   @{attributes [nitpick_psimp]}
 
-fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-
 fun note_qualified suffix attrs (fname, thms) =
   Local_Theory.note ((Binding.qualify true fname (Binding.name suffix),
     map (Attrib.internal o K) attrs), thms)
@@ -80,12 +78,14 @@
 
 fun prepare_function do_print prep fixspec eqns config lthy =
   let
-    val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy;
-    val fixes = map (apfst (apfst Binding.name_of)) fixes0;
-    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
+    val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy
+    val fixes = map (apfst (apfst Binding.name_of)) fixes0
+    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
 
-    val defname = mk_defname fixes
+    val fnames = map (fst o fst) fixes
+    val defname = space_implode "_" fnames
+
     val FunctionConfig {partials, default, ...} = config
     val _ =
       if is_some default
@@ -103,7 +103,6 @@
 
         val pelims = Function_Elims.mk_partial_elim_rules lthy result
 
-        val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
           |> Binding.qualify true defname
         val concealed_partial = if partials then I else Binding.concealed