src/Pure/Syntax/lexicon.ML
changeset 69344 f87fdd8d2baf
parent 69320 fc221fa79741
child 69891 def3ec9cdb7e
equal deleted inserted replaced
69343:395c4fb15ea2 69344:f87fdd8d2baf
    72 end;
    72 end;
    73 
    73 
    74 structure Lexicon: LEXICON =
    74 structure Lexicon: LEXICON =
    75 struct
    75 struct
    76 
    76 
    77 (** syntaxtic terms **)
    77 (** syntactic terms **)
    78 
    78 
    79 structure Syntax =
    79 structure Syntax =
    80 struct
    80 struct
    81 
    81 
    82 fun const c = Const (c, dummyT);
    82 fun const c = Const (c, dummyT);