Mutables in core code.

I looked up most of the mutables in the core code and listed them here. The ones that act like global variables are the ones I added. If the mutable looked like it was contained within a function such as a printing function then I did not add it here.

// Lib module  

(* ------------------------------------------------------------------------- *)
(* Flags to switch on verbose mode.                                          *)
(* ------------------------------------------------------------------------- *)

let verbose = ref true
let report_timing = ref true

// fusion.Hol_kernel module

    (* ------------------------------------------------------------------------- *)
    (* List of current type constants with their arities.                        *)
    (*                                                                           *)
    (* Initially we just have the boolean type and the function space            *)
    (* constructor. Later on we add as primitive the type of individuals.        *)
    (* All other new types result from definitional extension.                   *)
    (* ------------------------------------------------------------------------- *)

    let the_type_constants = 
        ref ["bool", 0;
             "fun", 2]

    (* ------------------------------------------------------------------------- *)
    (* List of term constants and their types.                                   *)
    (*                                                                           *)
    (* We begin with just equality (over all types). Later, the Hilbert choice   *)
    (* operator is added. All other new constants are defined.                   *)
    (* ------------------------------------------------------------------------- *)

    let the_term_constants = 
        ref ["=", Tyapp("fun", [aty;
                                Tyapp("fun", [aty; bool_ty])])]


// basics module

(* ------------------------------------------------------------------------- *)
(* Create probably-fresh variable                                            *)
(* ------------------------------------------------------------------------- *)

let genvar = 
    let gcounter = ref 0
    fun ty -> 
        let count = !gcounter
        gcounter := count + 1
        mk_var("_" + (string count), ty)

// printer module

(* ------------------------------------------------------------------------- *)
(* Reserved words.                                                           *)
(* ------------------------------------------------------------------------- *)

let reserve_words, unreserve_words, is_reserved_word, reserved_words = 
    let reswords = 
        ref ["(";
             ")";
             "[";
             "]";
             "{";
             "}";
             ":";
             ";";
             ".";
             "|";
             "let";
             "in";
             "and";
             "if";
             "then";
             "else";
             "match";
             "with";
             "function";
             "->";
             "when"]
    (fun ns -> reswords := union (!reswords) ns), (fun ns -> reswords := subtract (!reswords) ns), 
    (fun n -> mem n (!reswords)), (fun () -> !reswords)

(* ------------------------------------------------------------------------- *)
(* Flag determining whether interface/overloading is reversed on printing.   *)
(* ------------------------------------------------------------------------- *)

let reverse_interface_mapping = ref true

(* ------------------------------------------------------------------------- *)
(* Determine binary operators that print without surrounding spaces.         *)
(* ------------------------------------------------------------------------- *)

let unspaced_binops = 
    ref [",";
         "..";
         "$"]

(* ------------------------------------------------------------------------- *)
(* Binary operators to print at start of line when breaking.                 *)
(* ------------------------------------------------------------------------- *)

let prebroken_binops = ref ["==>"]

(* ------------------------------------------------------------------------- *)
(* Force explicit indications of bound variables in set abstractions.        *)
(* ------------------------------------------------------------------------- *)

let print_unambiguous_comprehensions = ref false

(* ------------------------------------------------------------------------- *)
(* Print the universal set UNIV:A->bool as "(:A)".                           *)
(* ------------------------------------------------------------------------- *)

let typify_universal_set = ref true
(* ------------------------------------------------------------------------- *)
(* Flag controlling whether hypotheses print.                                *)
(* ------------------------------------------------------------------------- *)

let print_all_thm = ref true

// preterm module

(* ------------------------------------------------------------------------- *)
(* Flag to say whether to treat varstruct "\const. bod" as variable.         *)
(* ------------------------------------------------------------------------- *)

let ignore_constant_varstruct = ref true

(* ------------------------------------------------------------------------- *)
(* Flags controlling the treatment of invented type variables in quotations. *)
(* It can be treated as an error, result in a warning, ||  neither of those.  *)
(* ------------------------------------------------------------------------- *)

let type_invention_warning = ref true
let type_invention_error = ref false

(* ------------------------------------------------------------------------- *)
(* Implicit types ||  type schemes for non-constants.                         *)
(* ------------------------------------------------------------------------- *)

let the_implicit_types = ref([] : (string * hol_type) list)


    (* ----------------------------------------------------------------------- *)
    (* Flag to indicate that Stvs were translated to real type variables.      *)
    (* ----------------------------------------------------------------------- *)

    let stvs_translated = ref false

// ind_defs module

(* ------------------------------------------------------------------------- *)
(* Assignable list of monotonicity theorems, so users can add their own.     *)
(* ------------------------------------------------------------------------- *)
let monotonicity_theorems = 
    ref [MONO_AND; MONO_OR; MONO_IMP; MONO_NOT; MONO_EXISTS; MONO_FORALL]

(* ========================================================================= *)
(* Part 3: The final user wrapper, with schematic variables added.           *)
(* ========================================================================= *)
let the_inductive_definitions = ref []

// class module

let inductive_type_store = ref ["bool", (2, bool_INDUCT, bool_RECURSION)]

// meson module

(* ------------------------------------------------------------------------- *)
(* Some parameters controlling MESON behaviour.                              *)
(* ------------------------------------------------------------------------- *)

let meson_depth = ref false   (* Use depth not inference bound.            *)

let meson_prefine = ref true  (* Use Plaisted's positive refinement.       *)

let meson_dcutin = ref 1      (* Min size for d-and-c optimization cut-in. *)

let meson_skew = ref 3        (* Skew proof bias (one side is <= n / skew) *)

let meson_brand = ref false   (* Use Brand transformation                  *)

let meson_split_limit = ref 8 (* Limit of case splits before MESON proper  *)

let meson_chatty = ref false  (* Old-style verbose MESON output            *)

// pair module

(* ------------------------------------------------------------------------- *)
(* Extend definitions to paired varstructs with benignity checking.          *)
(* ------------------------------------------------------------------------- *)
let the_definitions = 
    ref 
        [SND_DEF; FST_DEF; COMMA_DEF; mk_pair_def; GEQ_DEF; GABS_DEF; 
         LET_END_DEF; LET_DEF; one_DEF; I_DEF; o_DEF; COND_DEF; _FALSITY_; 
         EXISTS_UNIQUE_DEF; NOT_DEF; F_DEF; OR_DEF; EXISTS_DEF; FORALL_DEF; 
         IMP_DEF; AND_DEF; T_DEF]

// nums module

let the_specifications = ref []

// ind_types module

(* ------------------------------------------------------------------------- *)
(* Also add a cached rewrite of distinctness and injectivity theorems. Since *)
(* there can be quadratically many distinctness clauses, it would really be  *)
(* preferable to have a conversion, but this seems OK up 100 constructors.   *)
(* ------------------------------------------------------------------------- *)
let basic_rectype_net = ref empty_net

let distinctness_store = ref ["bool", TAUT(parse_term @"(T <=> F) <=> F")]
let injectivity_store = ref []

(* ----------------------------------------------------------------------- *)
(* The overall function, with rather crude string-based benignity.         *)
(* ----------------------------------------------------------------------- *)
let the_inductive_types = 
    ref ["list = NIL | CONS A list", (list_INDUCT, list_RECURSION)
         "option = NONE | SOME A", (option_INDUCT, option_RECURSION)
         "sum = INL A | INR B", (sum_INDUCT, sum_RECURSION)]