renamed "symbolfont" to "symbols";
authorwenzelm
Wed, 27 Nov 1996 16:36:36 +0100
changeset 2252 d54af138f7b2
parent 2251 e0e3836f333d
child 2253 95b615550b8b
renamed "symbolfont" to "symbols";
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)),