changeset 63120 | 629a4c5e953e |
parent 62900 | c641bf9402fd |
child 66067 | cdbcb417db67 |
--- a/src/Pure/ML/ml_thms.ML Mon May 23 20:45:10 2016 +0200 +++ b/src/Pure/ML/ml_thms.ML Mon May 23 21:30:30 2016 +0200 @@ -77,7 +77,7 @@ val and_ = Args.$$$ "and"; val by = Parse.reserved "by"; -val goal = Scan.unless (by || and_) Args.name_inner_syntax; +val goal = Scan.unless (by || and_) Args.embedded_inner_syntax; val _ = Theory.setup (ML_Antiquotation.declaration @{binding lemma}