src/Pure/Syntax/syntax.ML

     (string * (ast list -> ast)) list -> syntax
   val extend_trrules: syntax ->
     (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax
   val merge_syntaxes: syntax -> syntax -> syntax
   val type_syn: syntax
+  val pure_syn: syntax
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
   val test_read: syntax -> string -> string -> unit
   val read: syntax -> typ -> string -> term list

 (** datatype syntax **)
 
 datatype syntax =
   Syntax of {
     lexicon: lexicon,
-    roots: string list,
+    logtypes: string list,
     gram: gram,
     consts: string list,
     parse_ast_trtab: ast trtab,
     parse_ruletab: ruletab,
     parse_trtab: term trtab,

 (* empty_syntax *)
 
 val empty_syntax =
   Syntax {
     lexicon = empty_lexicon,
-    roots = [],
+    logtypes = [],
     gram = empty_gram,
     consts = [],
     parse_ast_trtab = empty_trtab,
     parse_ruletab = empty_ruletab,
     parse_trtab = empty_trtab,

 
 (* extend_syntax *)
 
 fun extend_syntax (Syntax tabs) syn_ext =
   let
-    val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
+    val {lexicon, logtypes = logtypes1, gram, consts = consts1, parse_ast_trtab,
       parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab,
       prtab} = tabs;
-    val SynExt {roots = roots2, xprods, consts = consts2, parse_ast_translation,
+    val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
       parse_rules, parse_translation, print_translation, print_rules,
       print_ast_translation} = syn_ext;
   in
     Syntax {
       lexicon = extend_lexicon lexicon (delims_of xprods),
-      roots = extend_list roots1 roots2,
-      gram = extend_gram gram (roots1 @ roots2) xprods,
+      logtypes = extend_list logtypes1 logtypes2,
+      gram = extend_gram gram (logtypes1 @ logtypes2) xprods,
       consts = consts2 union consts1,
       parse_ast_trtab =
         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
       parse_ruletab = extend_ruletab parse_ruletab parse_rules,
       parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",

 
 (* merge_syntaxes *)
 
 fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
   let
-    val {lexicon = lexicon1, roots = roots1, gram = gram1, consts = consts1,
+    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
       parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
       parse_trtab = parse_trtab1, print_trtab = print_trtab1,
       print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
       prtab = prtab1} = tabs1;
 
-    val {lexicon = lexicon2, roots = roots2, gram = gram2, consts = consts2,
+    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
       parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
       parse_trtab = parse_trtab2, print_trtab = print_trtab2,
       print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
       prtab = prtab2} = tabs2;
   in
     Syntax {
       lexicon = merge_lexicons lexicon1 lexicon2,
-      roots = merge_lists roots1 roots2,
+      logtypes = merge_lists logtypes1 logtypes2,
       gram = merge_grams gram1 gram2,
       consts = merge_lists consts1 consts2,
       parse_ast_trtab =
         merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation",
       parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,

 
 
 (* type_syn *)
 
 val type_syn = extend_syntax empty_syntax type_ext;
-
+val pure_syn = extend_syntax type_syn pure_ext;
 
 
 (** inspect syntax **)
 
 fun pretty_strs_qs name strs =

 
 (* print_gram *)
 
 fun print_gram (Syntax tabs) =
   let
-    val {lexicon, roots, gram, ...} = tabs;
+    val {lexicon, logtypes, gram, ...} = tabs;
   in
     Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
-    Pretty.writeln (Pretty.strs ("roots:" :: roots));
+    Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
     Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram))
   end;
 
 
 (* print_trans *)

 
 (* read_ast *)
 
 fun read_asts (Syntax tabs) print_msg xids root str =
   let
-    val {lexicon, gram, parse_ast_trtab, roots, ...} = tabs;
-    val root' = if root mem (roots \\ ["type", "prop"]) then "@logic_H"
-                else if root = "prop" then "@prop_H" else root;
+    val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
+    val root' = if root mem logtypes then logic else root;
     val pts = parse gram root' (tokenize lexicon xids str);
 
     fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   in
     if print_msg andalso length pts > 1 then

 
 
 
 (** extend syntax (external interfaces) **)
 
-fun ext_syntax mk_syn_ext (syn as Syntax {roots, ...}) decls =
-  extend_syntax syn (mk_syn_ext roots decls);
-
-
-fun extend_log_types (syn as Syntax {roots, ...}) all_roots =
-  extend_syntax syn (syn_ext_roots all_roots (all_roots \\ roots));
+fun ext_syntax mk_syn_ext (syn as Syntax {logtypes, ...}) decls =
+  extend_syntax syn (mk_syn_ext logtypes decls);
+
+
+fun extend_log_types syn logtypes =
+  extend_syntax syn (syn_ext_logtypes logtypes);
 
 val extend_type_gram = ext_syntax syn_ext_types;
 
 val extend_const_gram = ext_syntax syn_ext_consts;