let keyword =
  let kw_table = Hashtbl.create 31 in
  List.iter 
    (fun (s,tk) -> Hashtbl.add kw_table s tk)
    [ "arith", ARITH; "tuple", TUPLE;
      "in", IN; "inf", INF;
      "bot", BOT; "int", INT; "real", REAL; "top", TOP;
      "bitvector", BV; "with", WITH;
      "proj", PROJ;
      "cons", CONS; "car", CAR; "cdr", CDR;
      "conc", CONC; "sub", SUB; "ite", BWITE;
      "drop", DROP; "can", CAN; "assert", ASSERT; "exit", EXIT; 
      "valid", VALID; "unsat", UNSAT;
      "save", SAVE; "restore", RESTORE; "remove", REMOVE; "forget", FORGET;
      "reset", RESET; "sig", SIG; "type", TYPE; "def", DEF; "prop", PROP;
      "sigma", SIGMA; "solve", SOLVE; "help", HELP; "model", MODEL;
      "set", SET; "toggle", TOGGLE; "trace", TRACE;  "untrace", UNTRACE; 
      "find", FIND; "inv", INV; "use", USE; "solution", SOLUTION; "partition", PARTITION;
      "syntax", SYNTAX; "commands", COMMANDS; "ctxt", CTXT; "diseq", DISEQ; "echo", ECHO;
      "show", SHOW; "symtab", SYMTAB; "sign", SIGN; "dom", DOM; "split", SPLIT; "sat", SAT;
      "true", TRUE; "false", FALSE;
      "tt", TT; "ff", FF;
      "inr", INR; "inl", INL; "outr", OUTR; "outl", OUTL;
      "inj", INJ; "out", OUT;
      "hd", HEAD; "tl", TAIL;
      "unsigned", UNSIGNED; "apply", APPLY;
      "lambda", LAMBDA;
      "if", IF; "then", THEN; "else", ELSE; "end", END;
      "create", CREATE
    ];
  fun s ->
    try Hashtbl.find kw_table s with Not_found -> IDENT s