# HG changeset patch
# User wenzelm
# Date 1291212159 -3600
# Node ID b254814a094c9c42cafb75a2f51cea5a10ceb2c2
# Parent  6c7d2a8761ed61cb09ad9b468cfb98f40519dd14
tuned;

diff -r 6c7d2a8761ed -r b254814a094c src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Dec 01 14:56:07 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Dec 01 15:02:39 2010 +0100
@@ -81,7 +81,7 @@
 (* TODO: does not work with higher order functions yet *)
 fun mk_rewr_eq (func, pred) =
   let
-    val (argTs, resT) = (strip_type (fastype_of func))
+    val (argTs, resT) = strip_type (fastype_of func)
     val nctxt =
       Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
     val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt