changed Pure's grammar and the way types are converted to nonterminals
authorclasohm
Thu Dec 08 12:46:25 1994 +0100 (1994-12-08)
changeset 764b60e77395d1a
parent 763 d5a626aacdd3
child 765 06a484afc603
changed Pure's grammar and the way types are converted to nonterminals
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Thu Dec 08 12:45:28 1994 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Thu Dec 08 12:46:25 1994 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4  
     1.5  (* syn_ext_types *)
     1.6  
     1.7 -fun syn_ext_types all_roots type_decls =
     1.8 +fun syn_ext_types logtypes type_decls =
     1.9    let
    1.10      fun name_of (t, _, mx) = type_name t mx;
    1.11  
    1.12 @@ -95,13 +95,13 @@
    1.13      val mfix = mapfilter mfix_of type_decls;
    1.14      val xconsts = map name_of type_decls;
    1.15    in
    1.16 -    syn_ext all_roots [] mfix xconsts ([], [], [], []) ([], [])
    1.17 +    syn_ext logtypes mfix xconsts ([], [], [], []) ([], [])
    1.18    end;
    1.19  
    1.20  
    1.21  (* syn_ext_consts *)
    1.22  
    1.23 -fun syn_ext_consts all_roots const_decls =
    1.24 +fun syn_ext_consts logtypes const_decls =
    1.25    let
    1.26      fun name_of (c, _, mx) = const_name c mx;
    1.27  
    1.28 @@ -130,7 +130,7 @@
    1.29      val binder_trs = map mk_binder_tr binders;
    1.30      val binder_trs' = map (mk_binder_tr' o swap) binders;
    1.31    in
    1.32 -    syn_ext all_roots [] mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    1.33 +    syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    1.34    end;
    1.35  
    1.36  
    1.37 @@ -140,7 +140,7 @@
    1.38  val pure_types =
    1.39    map (fn t => (t, 0, NoSyn))
    1.40      (terminals @ [logic, "type", "types", "sort", "classes", args, "idt",
    1.41 -      "idts", "aprop", "asms", "any"]);
    1.42 +      "idts", "aprop", "asms"]);
    1.43  
    1.44  val pure_syntax =
    1.45   [("_lambda",   "[idts, 'a] => ('b => 'a)",       Mixfix ("(3%_./ _)", [], 0)),
    1.46 @@ -163,7 +163,6 @@
    1.47    ("_K",        "'a",                             NoSyn),
    1.48    ("",          "id => logic",                    Delimfix "_"),
    1.49    ("",          "var => logic",                   Delimfix "_"),
    1.50 -  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
    1.51 -  ("_constrain", "[logic, type] => logic",        Mixfix ("_::_", [4, 0], 3))]
    1.52 +  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))]
    1.53  
    1.54  end;
     2.1 --- a/src/Pure/Syntax/parser.ML	Thu Dec 08 12:45:28 1994 +0100
     2.2 +++ b/src/Pure/Syntax/parser.ML	Thu Dec 08 12:46:25 1994 +0100
     2.3 @@ -260,40 +260,15 @@
     2.4  
     2.5  fun extend_gram (gram1 as Gram (prods1, _)) roots xprods2 =
     2.6    let
     2.7 -    fun simplify preserve s = 
     2.8 -      if preserve then 
     2.9 -        (if s mem (roots \\ ["type", "prop", "any"]) then "logic" else s)
    2.10 -      else (if s = "prop" then "@prop_H" else
    2.11 -              (if s mem (roots \\ ["type", "prop", "any"]) then 
    2.12 -                 "@logic_H" 
    2.13 -               else s));
    2.14 -
    2.15 -    fun not_delim (Delim _) = false
    2.16 -      | not_delim _ = true
    2.17 -
    2.18 -    fun symb_of _ (Delim s) = Some (Terminal (Token s))
    2.19 -      | symb_of preserve (Argument (s, p)) =
    2.20 +    fun symb_of (Delim s) = Some (Terminal (Token s))
    2.21 +      | symb_of (Argument (s, p)) =
    2.22            (case predef_term s of
    2.23 -            None => Some (Nonterminal (simplify preserve s, p))
    2.24 +            None => Some (Nonterminal (s, p))
    2.25            | Some tk => Some (Terminal tk))
    2.26 -      | symb_of _ _ = None;
    2.27 +      | symb_of _ = None;
    2.28  
    2.29      fun prod_of (XProd (lhs, xsymbs, const, pri)) =
    2.30 -      let val copy_prod = (lhs = "prop" andalso forall not_delim xsymbs andalso
    2.31 -                           const <> "");
    2.32 -
    2.33 -          val preserve = copy_prod 
    2.34 -                         orelse pri = chain_pri andalso lhs = "logic"
    2.35 -                         orelse lhs mem ["@prop_H", "@logic_H", "any"];
    2.36 -
    2.37 -          val lhs' = if copy_prod then "@prop_H" else
    2.38 -                     if lhs = "logic" andalso pri = chain_pri
    2.39 -                        then "@logic_H"
    2.40 -                     else if lhs mem ("logic1" :: (roots \\ ["type", "prop"])) 
    2.41 -                        then "logic"
    2.42 -                     else lhs;
    2.43 -      in (lhs', (mapfilter (symb_of preserve) xsymbs, const, pri))
    2.44 -      end;
    2.45 +      (lhs, (mapfilter symb_of xsymbs, const, pri));
    2.46  
    2.47      val prods2 = distinct (map prod_of xprods2);
    2.48    in
    2.49 @@ -583,10 +558,6 @@
    2.50  
    2.51  fun earley grammar startsymbol indata =
    2.52    let
    2.53 -    val startsymbol' = case startsymbol of
    2.54 -                           "logic" => "@logic_H"
    2.55 -                         | "prop"  => "@prop_H"
    2.56 -                         | other   => other;
    2.57      val rhss_ref = case assoc (grammar, startsymbol) of
    2.58                         Some r => r
    2.59                       | None   => error ("parse: Unknown startsymbol " ^ 
     3.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Dec 08 12:45:28 1994 +0100
     3.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Dec 08 12:46:25 1994 +0100
     3.3 @@ -32,7 +32,7 @@
     3.4      datatype mfix = Mfix of string * typ * string * int list * int
     3.5      datatype syn_ext =
     3.6        SynExt of {
     3.7 -        roots: string list,
     3.8 +        logtypes: string list,
     3.9          xprods: xprod list,
    3.10          consts: string list,
    3.11          parse_ast_translation: (string * (ast list -> ast)) list,
    3.12 @@ -41,17 +41,23 @@
    3.13          print_translation: (string * (term list -> term)) list,
    3.14          print_rules: (ast * ast) list,
    3.15          print_ast_translation: (string * (ast list -> ast)) list}
    3.16 -    val syn_ext: string list -> string list -> mfix list -> string list ->
    3.17 +    val mk_syn_ext: bool -> string list -> mfix list ->
    3.18 +      string list -> (string * (ast list -> ast)) list * 
    3.19 +      (string * (term list -> term)) list *
    3.20 +      (string * (term list -> term)) list * (string * (ast list -> ast)) list
    3.21 +      -> (ast * ast) list * (ast * ast) list -> syn_ext
    3.22 +    val syn_ext: string list -> mfix list -> string list ->
    3.23        (string * (ast list -> ast)) list * (string * (term list -> term)) list *
    3.24        (string * (term list -> term)) list * (string * (ast list -> ast)) list
    3.25        -> (ast * ast) list * (ast * ast) list -> syn_ext
    3.26 -    val syn_ext_roots: string list -> string list -> syn_ext
    3.27 +    val syn_ext_logtypes: string list -> syn_ext
    3.28      val syn_ext_const_names: string list -> string list -> syn_ext
    3.29      val syn_ext_rules: string list -> (ast * ast) list * (ast * ast) list -> syn_ext
    3.30      val syn_ext_trfuns: string list ->
    3.31        (string * (ast list -> ast)) list * (string * (term list -> term)) list *
    3.32        (string * (term list -> term)) list * (string * (ast list -> ast)) list
    3.33        -> syn_ext
    3.34 +    val pure_ext: syn_ext
    3.35    end
    3.36  end;
    3.37  
    3.38 @@ -70,19 +76,18 @@
    3.39  val logicT = Type (logic, []);
    3.40  
    3.41  val logic1 = "logic1";
    3.42 -val logic1T = Type (logic1, []);
    3.43  
    3.44  val args = "args";
    3.45  val argsT = Type (args, []);
    3.46  
    3.47  val typeT = Type ("type", []);
    3.48  
    3.49 -val funT = Type ("fun", []);
    3.50 +val sprop = "#prop";
    3.51 +val spropT = Type (sprop, []);
    3.52  
    3.53 -val any = "any"
    3.54 +val any = "any";
    3.55  val anyT = Type (any, []);
    3.56  
    3.57 -
    3.58  (* constants *)
    3.59  
    3.60  val applC = "_appl";
    3.61 @@ -145,19 +150,22 @@
    3.62  
    3.63  (* typ_to_nonterm *)
    3.64  
    3.65 -fun typ_to_nonterm (Type (c, _)) = c
    3.66 +(*get nonterminal for rhs*)
    3.67 +fun typ_to_nonterm (Type (c, _)) = if c="fun" then logic else c
    3.68    | typ_to_nonterm _ = any;
    3.69  
    3.70 -fun typ_to_nonterm1 (Type (c, _)) = c
    3.71 -  | typ_to_nonterm1 _ = logic1;
    3.72 +(*get nonterminal for lhs*)
    3.73 +fun typ_to_nonterm1 (ty as Type (c, _)) = typ_to_nonterm ty
    3.74 +  | typ_to_nonterm1 _ = logic;
    3.75  
    3.76  
    3.77  (* mfix_to_xprod *)
    3.78  
    3.79 -fun mfix_to_xprod (Mfix (sy, typ, const, pris, pri)) =
    3.80 +fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
    3.81    let
    3.82      fun err msg =
    3.83 -      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
    3.84 +      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " 
    3.85 +                ^ quote const);
    3.86          error msg);
    3.87  
    3.88      fun check_pri p =
    3.89 @@ -218,21 +226,37 @@
    3.90      fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
    3.91        | rem_pri sym = sym;
    3.92  
    3.93 +    fun is_delim (Delim _) = true
    3.94 +      | is_delim _ = false;
    3.95 +
    3.96 +    (*replace logical types on rhs by "logic"*)
    3.97 +    fun unify_logtypes copy_prod (a as (Argument (s, p))) =
    3.98 +          if s mem logtypes then Argument (logic, p)
    3.99 +          else a
   3.100 +      | unify_logtypes _ a = a;
   3.101  
   3.102      val (raw_symbs, _) = repeat scan_symb (explode sy);
   3.103      val (symbs, lhs) = add_args raw_symbs typ pris;
   3.104 -    val xprod = XProd (lhs, symbs, const, pri);
   3.105 +    val copy_prod = lhs mem ["prop", "logic"]
   3.106 +          andalso const <> ""
   3.107 +          andalso not (exists is_delim symbs);
   3.108 +    val lhs' = if convert andalso not copy_prod then
   3.109 +                 (if lhs mem logtypes then logic
   3.110 +                  else if lhs = "prop" then sprop else lhs)
   3.111 +               else lhs;
   3.112 +    val symbs' = map (unify_logtypes copy_prod) symbs;
   3.113 +    val xprod = XProd (lhs', symbs', const, pri);
   3.114    in
   3.115      seq check_pri pris;
   3.116      check_pri pri;
   3.117 -    check_blocks symbs;
   3.118 +    check_blocks symbs';
   3.119  
   3.120 -    if is_terminal lhs then err ("illegal lhs: " ^ lhs)
   3.121 +    if is_terminal lhs' then err ("illegal lhs: " ^ lhs')
   3.122      else if const <> "" then xprod
   3.123 -    else if length (filter is_arg symbs) <> 1 then
   3.124 +    else if length (filter is_arg symbs') <> 1 then
   3.125        err "copy production must have exactly one argument"
   3.126 -    else if exists is_term symbs then xprod
   3.127 -    else XProd (lhs, map rem_pri symbs, "", chain_pri)
   3.128 +    else if exists is_term symbs' then xprod
   3.129 +    else XProd (lhs', map rem_pri symbs', "", chain_pri)
   3.130    end;
   3.131  
   3.132  
   3.133 @@ -240,7 +264,7 @@
   3.134  
   3.135  datatype syn_ext =
   3.136    SynExt of {
   3.137 -    roots: string list,
   3.138 +    logtypes: string list,
   3.139      xprods: xprod list,
   3.140      consts: string list,
   3.141      parse_ast_translation: (string * (ast list -> ast)) list,
   3.142 @@ -253,31 +277,18 @@
   3.143  
   3.144  (* syn_ext *)
   3.145  
   3.146 -fun syn_ext all_roots new_roots mfixes consts trfuns rules =
   3.147 +fun mk_syn_ext convert logtypes mfixes consts trfuns rules =
   3.148    let
   3.149      val (parse_ast_translation, parse_translation, print_translation,
   3.150        print_ast_translation) = trfuns;
   3.151      val (parse_rules, print_rules) = rules;
   3.152 +    val logtypes' = logtypes \ "prop";
   3.153  
   3.154      val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes);
   3.155 -    val mfixes' = (if "prop" mem new_roots then
   3.156 -                     [Mfix ("'(_')", Type ("@prop_H", [])
   3.157 -                            --> Type ("@prop_H", []), "", [0], max_pri),
   3.158 -                      Mfix ("'(_')", Type ("@logic_H", []) 
   3.159 -                            --> Type ("@logic_H", []), "", [0], max_pri),
   3.160 -                      Mfix ("'(_')", anyT --> anyT, "", [0], max_pri),
   3.161 -                      Mfix ("_", propT --> Type ("@prop_H", []), "", [0], 0),
   3.162 -                      Mfix ("_", propT --> anyT, "", [0], 0)]
   3.163 -                   else []) @
   3.164 -                   (if all_roots = new_roots then
   3.165 -                     [Mfix ("_", logicT --> Type ("@logic_H", []), "", [0], 0),
   3.166 -                      Mfix ("_", logicT --> anyT, "", [0], 0)]
   3.167 -                    else [])    
   3.168 -    val xprods = map mfix_to_xprod mfixes 
   3.169 -                 @ map mfix_to_xprod mfixes';
   3.170 +    val xprods = map (mfix_to_xprod convert logtypes') mfixes;
   3.171    in
   3.172      SynExt {
   3.173 -      roots = new_roots,
   3.174 +      logtypes = logtypes',
   3.175        xprods = xprods,
   3.176        consts = filter is_xid (consts union mfix_consts),
   3.177        parse_ast_translation = parse_ast_translation,
   3.178 @@ -288,18 +299,32 @@
   3.179        print_ast_translation = print_ast_translation}
   3.180    end;
   3.181  
   3.182 +val syn_ext = mk_syn_ext true;
   3.183  
   3.184 -fun syn_ext_roots roots new_roots =
   3.185 -  syn_ext roots new_roots [] [] ([], [], [], []) ([], []);
   3.186 +fun syn_ext_logtypes logtypes =
   3.187 +  syn_ext logtypes [] [] ([], [], [], []) ([], []);
   3.188 +
   3.189 +fun syn_ext_const_names logtypes cs =
   3.190 +  syn_ext logtypes [] cs ([], [], [], []) ([], []);
   3.191  
   3.192 -fun syn_ext_const_names roots cs =
   3.193 -  syn_ext roots [] [] cs ([], [], [], []) ([], []);
   3.194 +fun syn_ext_rules logtypes rules =
   3.195 +  syn_ext logtypes [] [] ([], [], [], []) rules;
   3.196 +
   3.197 +fun syn_ext_trfuns logtypes trfuns =
   3.198 +  syn_ext logtypes [] [] trfuns ([], []);
   3.199  
   3.200 -fun syn_ext_rules roots rules =
   3.201 -  syn_ext roots [] [] [] ([], [], [], []) rules;
   3.202 +(* pure_ext *)
   3.203  
   3.204 -fun syn_ext_trfuns roots trfuns =
   3.205 -  syn_ext roots [] [] [] trfuns ([], []);
   3.206 -
   3.207 +val pure_ext = mk_syn_ext false []
   3.208 +  [Mfix ("_", spropT --> propT, "", [0], 0),
   3.209 +   Mfix ("_", logicT --> anyT, "", [0], 0),
   3.210 +   Mfix ("_", spropT --> anyT, "", [0], 0),
   3.211 +   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
   3.212 +   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
   3.213 +   Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
   3.214 +   Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
   3.215 +  []
   3.216 +  ([], [], [], [])
   3.217 +  ([], []);
   3.218  
   3.219  end;
     4.1 --- a/src/Pure/Syntax/syntax.ML	Thu Dec 08 12:45:28 1994 +0100
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Dec 08 12:46:25 1994 +0100
     4.3 @@ -47,6 +47,7 @@
     4.4      (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax
     4.5    val merge_syntaxes: syntax -> syntax -> syntax
     4.6    val type_syn: syntax
     4.7 +  val pure_syn: syntax
     4.8    val print_gram: syntax -> unit
     4.9    val print_trans: syntax -> unit
    4.10    val print_syntax: syntax -> unit
    4.11 @@ -134,7 +135,7 @@
    4.12  datatype syntax =
    4.13    Syntax of {
    4.14      lexicon: lexicon,
    4.15 -    roots: string list,
    4.16 +    logtypes: string list,
    4.17      gram: gram,
    4.18      consts: string list,
    4.19      parse_ast_trtab: ast trtab,
    4.20 @@ -151,7 +152,7 @@
    4.21  val empty_syntax =
    4.22    Syntax {
    4.23      lexicon = empty_lexicon,
    4.24 -    roots = [],
    4.25 +    logtypes = [],
    4.26      gram = empty_gram,
    4.27      consts = [],
    4.28      parse_ast_trtab = empty_trtab,
    4.29 @@ -167,17 +168,17 @@
    4.30  
    4.31  fun extend_syntax (Syntax tabs) syn_ext =
    4.32    let
    4.33 -    val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
    4.34 +    val {lexicon, logtypes = logtypes1, gram, consts = consts1, parse_ast_trtab,
    4.35        parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab,
    4.36        prtab} = tabs;
    4.37 -    val SynExt {roots = roots2, xprods, consts = consts2, parse_ast_translation,
    4.38 +    val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
    4.39        parse_rules, parse_translation, print_translation, print_rules,
    4.40        print_ast_translation} = syn_ext;
    4.41    in
    4.42      Syntax {
    4.43        lexicon = extend_lexicon lexicon (delims_of xprods),
    4.44 -      roots = extend_list roots1 roots2,
    4.45 -      gram = extend_gram gram (roots1 @ roots2) xprods,
    4.46 +      logtypes = extend_list logtypes1 logtypes2,
    4.47 +      gram = extend_gram gram (logtypes1 @ logtypes2) xprods,
    4.48        consts = consts2 union consts1,
    4.49        parse_ast_trtab =
    4.50          extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
    4.51 @@ -195,13 +196,13 @@
    4.52  
    4.53  fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
    4.54    let
    4.55 -    val {lexicon = lexicon1, roots = roots1, gram = gram1, consts = consts1,
    4.56 +    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
    4.57        parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
    4.58        parse_trtab = parse_trtab1, print_trtab = print_trtab1,
    4.59        print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
    4.60        prtab = prtab1} = tabs1;
    4.61  
    4.62 -    val {lexicon = lexicon2, roots = roots2, gram = gram2, consts = consts2,
    4.63 +    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
    4.64        parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
    4.65        parse_trtab = parse_trtab2, print_trtab = print_trtab2,
    4.66        print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
    4.67 @@ -209,7 +210,7 @@
    4.68    in
    4.69      Syntax {
    4.70        lexicon = merge_lexicons lexicon1 lexicon2,
    4.71 -      roots = merge_lists roots1 roots2,
    4.72 +      logtypes = merge_lists logtypes1 logtypes2,
    4.73        gram = merge_grams gram1 gram2,
    4.74        consts = merge_lists consts1 consts2,
    4.75        parse_ast_trtab =
    4.76 @@ -227,7 +228,7 @@
    4.77  (* type_syn *)
    4.78  
    4.79  val type_syn = extend_syntax empty_syntax type_ext;
    4.80 -
    4.81 +val pure_syn = extend_syntax type_syn pure_ext;
    4.82  
    4.83  
    4.84  (** inspect syntax **)
    4.85 @@ -240,10 +241,10 @@
    4.86  
    4.87  fun print_gram (Syntax tabs) =
    4.88    let
    4.89 -    val {lexicon, roots, gram, ...} = tabs;
    4.90 +    val {lexicon, logtypes, gram, ...} = tabs;
    4.91    in
    4.92      Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
    4.93 -    Pretty.writeln (Pretty.strs ("roots:" :: roots));
    4.94 +    Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
    4.95      Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram))
    4.96    end;
    4.97  
    4.98 @@ -304,9 +305,8 @@
    4.99  
   4.100  fun read_asts (Syntax tabs) print_msg xids root str =
   4.101    let
   4.102 -    val {lexicon, gram, parse_ast_trtab, roots, ...} = tabs;
   4.103 -    val root' = if root mem (roots \\ ["type", "prop"]) then "@logic_H"
   4.104 -                else if root = "prop" then "@prop_H" else root;
   4.105 +    val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
   4.106 +    val root' = if root mem logtypes then logic else root;
   4.107      val pts = parse gram root' (tokenize lexicon xids str);
   4.108  
   4.109      fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   4.110 @@ -436,12 +436,12 @@
   4.111  
   4.112  (** extend syntax (external interfaces) **)
   4.113  
   4.114 -fun ext_syntax mk_syn_ext (syn as Syntax {roots, ...}) decls =
   4.115 -  extend_syntax syn (mk_syn_ext roots decls);
   4.116 +fun ext_syntax mk_syn_ext (syn as Syntax {logtypes, ...}) decls =
   4.117 +  extend_syntax syn (mk_syn_ext logtypes decls);
   4.118  
   4.119  
   4.120 -fun extend_log_types (syn as Syntax {roots, ...}) all_roots =
   4.121 -  extend_syntax syn (syn_ext_roots all_roots (all_roots \\ roots));
   4.122 +fun extend_log_types syn logtypes =
   4.123 +  extend_syntax syn (syn_ext_logtypes logtypes);
   4.124  
   4.125  val extend_type_gram = ext_syntax syn_ext_types;
   4.126  
     5.1 --- a/src/Pure/Syntax/type_ext.ML	Thu Dec 08 12:45:28 1994 +0100
     5.2 +++ b/src/Pure/Syntax/type_ext.ML	Thu Dec 08 12:46:25 1994 +0100
     5.3 @@ -157,8 +157,7 @@
     5.4  val classesT = Type ("classes", []);
     5.5  val typesT = Type ("types", []);
     5.6  
     5.7 -val type_ext = syn_ext
     5.8 -  [logic, "type"] [logic, "type"]
     5.9 +val type_ext = mk_syn_ext false []
    5.10    [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    5.11     Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    5.12     Mfix ("_",           idT --> typeT,                 "", [], max_pri),
    5.13 @@ -185,4 +184,3 @@
    5.14  
    5.15  
    5.16  end;
    5.17 -