1.1 --- a/src/Pure/pure_thy.ML	Mon Nov 29 14:12:53 1999 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Mon Nov 29 15:52:49 1999 +0100
     1.3 @@ -435,11 +435,11 @@
     1.4      ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     1.5      ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     1.6      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     1.7 -    ("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
     1.8 +    ("Goal", "prop => prop", Mixfix ("GOAL _", [1000], 999)),
     1.9      ("TYPE", "'a itself", NoSyn),
    1.10      (dummy_patternN, "'a", Delimfix "'_")]
    1.11    |> Theory.add_modesyntax ("", false)
    1.12 -    [("Goal", "prop => prop", Mixfix ("_", [0], 1000))]
    1.13 +    [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
    1.14    |> local_path
    1.15    |> (add_defs o map Thm.no_attributes)
    1.16     [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),