1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 01 16:11:48 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 01 16:46:11 2010 +0200
     1.3 @@ -272,10 +272,7 @@
     1.4  val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
     1.5  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
     1.6  val parse_fact_refs =
     1.7 -  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
     1.8 -                            (Parse.xname -- Scan.option Attrib.thm_sel)
     1.9 -                >> (fn (name, interval) =>
    1.10 -                       Facts.Named ((name, Position.none), interval)))
    1.11 +  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
    1.12  val parse_relevance_chunk =
    1.13    (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
    1.14    || (Args.del |-- Args.colon |-- parse_fact_refs