diff -r f507e6fe1d77 -r d743bb1b6c23 src/HOL/Tools/Function/function_common.ML
--- 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 *)