src/HOL/Tools/Lifting/lifting_setup.ML
changeset 56035 745f568837f1
parent 56029 8bedca4bd5a3
child 56257 589fafcc7cb6
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 21:15:29 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 21:40:39 2014 +0100
@@ -958,12 +958,10 @@
   in
     case bundle of
       [(_, [arg_src])] => 
-        (let
-          val tokens = Args.args_of_src arg_src
-        in
-          (fst (Args.name tokens))
-          handle _ => error "The provided bundle is not a lifting bundle."
-        end)
+        let
+          val (name, _) = Args.syntax (Scan.lift Args.name) arg_src ctxt
+            handle ERROR _ => error "The provided bundle is not a lifting bundle."
+        in name end
       | _ => error "The provided bundle is not a lifting bundle."
   end