--- 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 *)