# HG changeset patch
# User wenzelm
# Date 1300971279 -3600
# Node ID 21697a5cb34acc12154c3f769988d2ccfda054c1
# Parent  58b465952287fa2512ae575976ef0fe9cd073b8e
indentation;

diff -r 58b465952287 -r 21697a5cb34a src/HOL/Tools/Function/function_common.ML
--- 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 ^