fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Sun Apr 22 14:16:46 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun Apr 22 16:53:24 2012 +0200
@@ -191,7 +191,7 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
-    val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
+    val transfer_thm = ([quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
         |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
 
     fun qualify defname suffix = Binding.qualified true suffix defname