--- a/src/HOL/Tools/try0.ML Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/try0.ML Thu Aug 21 22:48:39 2014 +0200
@@ -176,7 +176,7 @@
implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
val parse_fact_refs =
- Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
+ Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
val parse_attr =
Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], []))