# HG changeset patch
# User wenzelm
# Date 1460982402 -7200
# Node ID 8e03788644786a20bc373e1fff164f578b8075dc
# Parent  3c2df99b7b1dbac1036764ca26de6257188a548d
tuned;

diff -r 3c2df99b7b1d -r 8e0378864478 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon Apr 18 14:26:21 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Mon Apr 18 14:26:42 2016 +0200
@@ -69,7 +69,7 @@
     domintros: bool,
     partials: bool}
   type preproc = function_config -> Proof.context -> fixes -> term spec ->
-    (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
+    term list * (thm list -> thm spec) * (thm list -> thm list list) * string list
   val fname_of : term -> string
   val mk_case_names : int -> string -> int -> string list
   val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) ->
@@ -209,7 +209,7 @@
   partials: bool}
 
 type preproc = function_config -> Proof.context -> fixes -> term spec ->
-  (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
+  term list * (thm list -> thm spec) * (thm list -> thm list list) * string list
 
 val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
   HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all