src/HOL/Tools/Function/function_common.ML

         val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
 
         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 ^
            " occur" ^ plural "s" "" rvs ^ " on right hand side only:")