# HG changeset patch
# User wenzelm
# Date 1394484039 -3600
# Node ID 745f568837f18f8e50be0051e11ddf9220d01941
# Parent  1c59b555ac4acdc7841facb5e8647bc34b5f3d17
proper Args.syntax for slightly odd bundle trickery;
do not handle arbitrary exceptions;
more abstract type Args.src;

diff -r 1c59b555ac4a -r 745f568837f1 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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
 
diff -r 1c59b555ac4a -r 745f568837f1 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Mar 10 21:15:29 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 10 21:40:39 2014 +0100
@@ -10,7 +10,6 @@
   type src
   val src: xstring * Position.T -> Token.T list -> src
   val name_of_src: src -> string * Position.T
-  val args_of_src: src -> Token.T list
   val range_of_src: src -> Position.T
   val unparse_src: src -> string list
   val pretty_src: Proof.context -> src -> Pretty.T