diff -r d1ecc9cec531 -r 87c0eaf04bad src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 16:29:17 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 17:51:12 2012 +0200
@@ -177,7 +177,7 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
-    val transfer_thm = def_thm RS (rsp_thm RS (quotient_thm RS @{thm Quotient_to_transfer}))
+    val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
 
     fun qualify defname suffix = Binding.name suffix
       |> Binding.qualify true defname