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.
indentation;
authorwenzelm
Thu, 24 Mar 2011 13:54:39 +0100
changeset 42081 21697a5cb34a
parent 42080 58b465952287
child 42082 47f8bfe0f597
indentation;
src/HOL/Tools/Function/function_common.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/function_common.ML	Thu Mar 24 11:45:39 2011 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Mar 24 13:54:39 2011 +0100
@@ -243,8 +243,8 @@
         val _ = length args > 0 orelse input_error "Function has no arguments:"
 
         fun add_bvs t is = add_loose_bnos (t, 0, is)
-            val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
-                        |> map (fst o nth (rev qs))
+        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
+                    |> map (fst o nth (rev qs))
 
         val _ = null rvs orelse input_error
           ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
isabelle