| changeset 58028 | e4250d370657 |
| parent 58011 | bc6bced136e5 |
| child 58843 | 521cea5fa777 |
--- a/src/Pure/Isar/calculation.ML Thu Aug 21 13:46:29 2014 +0200 +++ b/src/Pure/Isar/calculation.ML Thu Aug 21 22:48:39 2014 +0200 @@ -201,7 +201,7 @@ (* outer syntax *) val calc_args = - Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"}))); + Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"}))); val _ = Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"