src/HOL/Tools/Lifting/lifting_setup.ML

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 23 17:18:18 2012 +0200
@@ -18,9 +18,9 @@
 structure Lifting_Setup: LIFTING_SETUP =
 struct
 
-infix 0 MRSL
+open Lifting_Util
 
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+infix 0 MRSL
 
 exception SETUP_LIFTING_INFR of string