Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Wed, 01 Dec 2010 15:02:39 +0100
changeset 40843 b254814a094c
parent 40842 6c7d2a8761ed
child 40844 5895c525739d
tuned;
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle