# HG changeset patch
# User wenzelm
# Date 1086086146 -7200
# Node ID a58abaad4f45d7c636ebfe4b26be3f490a659373
# Parent  61bdf2ae4dc59a829b6f9da818eb645c0aff9571
removed obsolete sort 'logic' and '=?=' syntax;

diff -r 61bdf2ae4dc5 -r a58abaad4f45 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Jun 01 12:33:50 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Jun 01 12:35:46 2004 +0200
@@ -266,10 +266,9 @@
   ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
   ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
   ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
-  ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
+  ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
-  ("=?=",      "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>\\<^sup>?", 2)),
   ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];