src/Pure/Syntax/mixfix.ML

   | const_name c _ = c;
 
 
 (* syn_ext_types *)
 
-fun syn_ext_types all_roots type_decls =
+fun syn_ext_types logtypes type_decls =
   let
     fun name_of (t, _, mx) = type_name t mx;
 
     fun mk_infix t p1 p2 p3 =
       Mfix ("(_ " ^ t ^ "/ _)", [typeT, typeT] ---> typeT,

           quote (name_of decl));
 
     val mfix = mapfilter mfix_of type_decls;
     val xconsts = map name_of type_decls;
   in
-    syn_ext all_roots [] mfix xconsts ([], [], [], []) ([], [])
+    syn_ext logtypes mfix xconsts ([], [], [], []) ([], [])
   end;
 
 
 (* syn_ext_consts *)
 
-fun syn_ext_consts all_roots const_decls =
+fun syn_ext_consts logtypes const_decls =
   let
     fun name_of (c, _, mx) = const_name c mx;
 
     fun mk_infix sy ty c p1 p2 p3 =
       [Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3),

     val xconsts = map name_of const_decls;
     val binders = mapfilter binder const_decls;
     val binder_trs = map mk_binder_tr binders;
     val binder_trs' = map (mk_binder_tr' o swap) binders;
   in
-    syn_ext all_roots [] mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
+    syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
   end;
 
 
 
 (** Pure syntax **)
 
 val pure_types =
   map (fn t => (t, 0, NoSyn))
     (terminals @ [logic, "type", "types", "sort", "classes", args, "idt",
-      "idts", "aprop", "asms", "any"]);
+      "idts", "aprop", "asms"]);
 
 val pure_syntax =
  [("_lambda",   "[idts, 'a] => ('b => 'a)",       Mixfix ("(3%_./ _)", [], 0)),
   ("",          "'a => " ^ args,                  Delimfix "_"),
   ("_args",     "['a, " ^ args ^ "] => " ^ args,  Delimfix "_,/ _"),

   ("_bigimpl",  "[asms, prop] => prop",           Mixfix ("((3[| _ |]) ==>/ _)", [0, 1], 1)),
   ("_ofclass",  "[type, 'a] => prop",             Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   ("_K",        "'a",                             NoSyn),
   ("",          "id => logic",                    Delimfix "_"),
   ("",          "var => logic",                   Delimfix "_"),
-  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
-  ("_constrain", "[logic, type] => logic",        Mixfix ("_::_", [4, 0], 3))]
+  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))]
 
 end;