src/Pure/Syntax/syntax.ML
changeset 35668 69e1740fbfb1
parent 35429 afa8cf9e63d8
child 36208 74c5e6e3c1d3
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Mar 09 14:55:25 2010 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Mar 09 14:29:47 2010 +0100
     1.3 @@ -29,10 +29,7 @@
     1.4    val mode_default: mode
     1.5    val mode_input: mode
     1.6    val merge_syntaxes: syntax -> syntax -> syntax
     1.7 -  val empty_syntax: syntax
     1.8 -  val basic_syntax:
     1.9 -   {read_class: theory -> xstring -> string,
    1.10 -    read_type: theory -> xstring -> string} -> syntax
    1.11 +  val basic_syntax: syntax
    1.12    val basic_nonterms: string list
    1.13    val print_gram: syntax -> unit
    1.14    val print_trans: syntax -> unit
    1.15 @@ -383,9 +380,9 @@
    1.16  
    1.17  (* basic syntax *)
    1.18  
    1.19 -fun basic_syntax read =
    1.20 +val basic_syntax =
    1.21    empty_syntax
    1.22 -  |> update_syntax mode_default (TypeExt.type_ext read)
    1.23 +  |> update_syntax mode_default TypeExt.type_ext
    1.24    |> update_syntax mode_default SynExt.pure_ext;
    1.25  
    1.26  val basic_nonterms =