--- 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