# HG changeset patch
# User wenzelm
# Date 849108996 -3600
# Node ID d54af138f7b2275e2309d60ad61eca68d1e61f8d
# Parent  e0e3836f333ddb3a42c5e9504cbc0caa6feef83e
renamed "symbolfont" to "symbols";

diff -r e0e3836f333d -r d54af138f7b2 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Nov 27 13:51:49 1996 +0100
+++ b/src/Pure/sign.ML	Wed Nov 27 16:36:36 1996 +0100
@@ -611,7 +611,7 @@
     ("prop", [], logicS),
     ("itself", [logicS], logicS)]
   |> add_syntax Syntax.pure_syntax
-  |> add_modesyntax ("symbolfont", Syntax.pure_symfont_syntax)
+  |> add_modesyntax ("symbols", Syntax.pure_sym_syntax)
   |> add_trfuns Syntax.pure_trfuns
   |> add_consts
    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),