diff -r 9a1212f4393e -r 9225bb0d1327 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Feb 16 20:44:25 2018 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Feb 16 21:33:04 2018 +0100
@@ -6,15 +6,13 @@
 
 signature FUNCTION =
 sig
-  include FUNCTION_DATA
-
   val add_function: (binding * typ option * mixfix) list ->
     Specification.multi_specs -> Function_Common.function_config ->
-    (Proof.context -> tactic) -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> local_theory -> Function_Common.info * local_theory
 
   val add_function_cmd: (binding * string option * mixfix) list ->
     Specification.multi_specs_cmd -> Function_Common.function_config ->
-    (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> bool -> local_theory -> Function_Common.info * local_theory
 
   val function: (binding * typ option * mixfix) list ->
     Specification.multi_specs -> Function_Common.function_config ->
@@ -25,16 +23,16 @@
     bool -> local_theory -> Proof.state
 
   val prove_termination: term option -> tactic -> local_theory ->
-    info * local_theory
+    Function_Common.info * local_theory
   val prove_termination_cmd: string option -> tactic -> local_theory ->
-    info * local_theory
+    Function_Common.info * local_theory
 
   val termination : term option -> local_theory -> Proof.state
   val termination_cmd : string option -> local_theory -> Proof.state
 
   val get_congs : Proof.context -> thm list
 
-  val get_info : Proof.context -> term -> info
+  val get_info : Proof.context -> term -> Function_Common.info
 end
 
 
@@ -266,7 +264,7 @@
 
 val get_congs = Function_Context_Tree.get_function_congs
 
-fun get_info ctxt t = Item_Net.retrieve (get_functions ctxt) t
+fun get_info ctxt t = Function_Common.retrieve_function_data ctxt t
   |> the_single |> snd