# HG changeset patch
# User huffman
# Date 1335106404 -7200
# Node ID 4483c004499ac7e93922e89f90cad2b8df8e491e
# Parent  1bf4fa90cd037e0360c642e1132a632a71c25715
fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)

diff -r 1bf4fa90cd03 -r 4483c004499a src/HOL/Tools/Lifting/lifting_def.ML
--- 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