# HG changeset patch
# User wenzelm
# Date 935059665 -7200
# Node ID da64f7413efd4dbb797c0de51170b472c57929c4
# Parent  bb9502f9154a0c85bfd5e1bd57cad4546bf4bb3f
tuned Goal syntax;

diff -r bb9502f9154a -r da64f7413efd src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Aug 19 12:43:02 1999 +0200
+++ b/src/Pure/pure_thy.ML	Thu Aug 19 12:47:45 1999 +0200
@@ -432,7 +432,7 @@
     ("TYPE", "'a itself", NoSyn),
     (dummy_patternN, "'a", Delimfix "'_")]
   |> Theory.add_modesyntax ("", false)
-    [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
+    [("Goal", "prop => prop", Mixfix ("_", [0], 1000))]
   |> local_path
   |> (add_defs o map Thm.no_attributes)
    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),