diff -r 422024102d9d -r 8bedca4bd5a3 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -223,7 +223,7 @@
     val dummy_thm = Thm.transfer thy Drule.dummy_thm
     val pointer = Outer_Syntax.scan Position.none bundle_name
     val restore_lifting_att = 
-      ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
+      ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
   in
     lthy 
       |> Local_Theory.declaration {syntax = false, pervasive = true}
@@ -959,7 +959,7 @@
     case bundle of
       [(_, [arg_src])] => 
         (let
-          val ((_, tokens), _) = Args.dest_src arg_src
+          val tokens = Args.args_of_src arg_src
         in
           (fst (Args.name tokens))
           handle _ => error "The provided bundle is not a lifting bundle."