diff -r dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/try0.ML
--- 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, [], [], []))