Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;

--- a/src/Pure/pure_thy.ML	Fri Nov 10 19:20:17 2000 +0100
+++ b/src/Pure/pure_thy.ML	Sun Nov 12 14:35:41 2000 +0100
@@ -478,7 +478,8 @@
     ("TYPE", "'a itself", NoSyn),
     (Term.dummy_patternN, "'a", Delimfix "'_")]
   |> Theory.add_modesyntax ("", false)
-    [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
+    (("Goal", "prop => prop", Mixfix ("_", [0], 0))
+      :: Syntax.pure_appl_syntax)
   |> local_path
   |> (#1 oo (add_defs false o map Thm.no_attributes))
    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),