1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -238,9 +238,9 @@
     1.4        (case try (unprefix "mono_") type_sys of
     1.5           SOME s => (true, s)
     1.6         | NONE => (false, type_sys))
     1.7 -      ||> (fn s => case try (unsuffix " **") s of
     1.8 +      ||> (fn s => case try (unsuffix " !!") s of
     1.9                       SOME s => (Unsound, s)
    1.10 -                   | NONE => case try (unsuffix " *") s of
    1.11 +                   | NONE => case try (unsuffix " !") s of
    1.12                                 SOME s => (Half_Sound, s)
    1.13                               | NONE => (Sound, s))
    1.14        |> (fn (mono, (level, core)) =>
    1.15 @@ -350,7 +350,9 @@
    1.16                    end))
    1.17  
    1.18  val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
    1.19 -val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number)
    1.20 +val parse_value =
    1.21 +  Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "!!"
    1.22 +                || Parse.$$$ "!")
    1.23  val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
    1.24  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
    1.25  val parse_fact_refs =