# HG changeset patch
# User wenzelm
# Date 943887169 -3600
# Node ID a901bafe4578c24385aad066b93e16c946b480e1
# Parent  a13c3b80d3d47a7524d4cf504ae2af55a5424772
Goal: tuned pris;

diff -r a13c3b80d3d4 -r a901bafe4578 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Nov 29 14:12:53 1999 +0100
+++ b/src/Pure/pure_thy.ML	Mon Nov 29 15:52:49 1999 +0100
@@ -435,11 +435,11 @@
     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
-    ("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
+    ("Goal", "prop => prop", Mixfix ("GOAL _", [1000], 999)),
     ("TYPE", "'a itself", NoSyn),
     (dummy_patternN, "'a", Delimfix "'_")]
   |> Theory.add_modesyntax ("", false)
-    [("Goal", "prop => prop", Mixfix ("_", [0], 1000))]
+    [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
   |> local_path
   |> (add_defs o map Thm.no_attributes)
    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),