# 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