author | wenzelm |
Wed, 19 Oct 2011 17:03:07 +0200 | |
changeset 45198 | f579dab96734 |
parent 45197 | b6c527c64789 |
child 45199 | 42316b81ef49 |
--- a/src/Pure/ML/ml_thms.ML Wed Oct 19 16:45:46 2011 +0200 +++ b/src/Pure/ML/ml_thms.ML Wed Oct 19 17:03:07 2011 +0200 @@ -52,7 +52,7 @@ val and_ = Args.$$$ "and"; val by = Args.$$$ "by"; -val goal = Scan.unless (by || and_) Args.name; +val goal = Scan.unless (by || and_) Args.name_source; val _ = Context.>> (Context.map_theory