# HG changeset patch
# User wenzelm
# Date 1518815810 -3600
# Node ID fb4b2b6333710a8c202f5328609f3b687d4680aa
# Parent  e6bcd14139fcbbb432ca97bad6ac919f75d94b19
tuned signature (again);

diff -r e6bcd14139fc -r fb4b2b633371 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Feb 16 22:11:59 2018 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Feb 16 22:16:50 2018 +0100
@@ -6,13 +6,15 @@
 
 signature FUNCTION =
 sig
+  type info = Function_Common.info
+
   val add_function: (binding * typ option * mixfix) list ->
     Specification.multi_specs -> Function_Common.function_config ->
-    (Proof.context -> tactic) -> local_theory -> Function_Common.info * local_theory
+    (Proof.context -> tactic) -> local_theory -> 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 -> Function_Common.info * local_theory
+    (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
 
   val function: (binding * typ option * mixfix) list ->
     Specification.multi_specs -> Function_Common.function_config ->
@@ -23,16 +25,16 @@
     bool -> local_theory -> Proof.state
 
   val prove_termination: term option -> tactic -> local_theory ->
-    Function_Common.info * local_theory
+    info * local_theory
   val prove_termination_cmd: string option -> tactic -> local_theory ->
-    Function_Common.info * local_theory
+    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 -> Function_Common.info
+  val get_info : Proof.context -> term -> info
 end