Fix a crash in loading update_database.ml

This fixes a crash in loading update_database.ml after #74.

The newly written update_database.ml is largely based on @chetmurthy's work:

https://github.com/chetmurthy/hol-light/blob/99d017c087ee938929d9d40a5fe75022bbee0257/update_database_6.ml

... with the following modification to address updates in OCaml's Types module as well as crashes when deprecated stdlib modules are to be loaded:

diff --git a/update_database_4.14.ml b/update_database_4.14.ml
index 79bc6fc..c2b69d4 100755
--- a/update_database_4.14.ml
+++ b/update_database_4.14.ml
@@ -17,9 +17,11 @@ open Types
 (* If the given type is simple return its name, otherwise None. *)

 let rec get_simple_type = function
-  | Tlink { desc = Tconstr (Pident p,[],_) } -> Some (Ident.name p)
+  | Tlink texpr ->
+    (match get_desc texpr with
+    | Tconstr (Pident p,[],_) -> Some (Ident.name p)
+    | d -> get_simple_type d)
   | Tconstr (Path.Pident p,  [], _) -> Some (Ident.name p)
-  | Tlink { desc = d } -> get_simple_type d
   | _ -> None;;

 (* Execute any OCaml expression given as a string. *)
@@ -45,15 +47,22 @@ let lid_cons lidopt id =
   | Some li -> Longident.Ldot(li, id)

 let it_val_1 lidopt s p vd acc =
-  if (Some "thm") = Ocaml_typing.get_simple_type vd.Types.val_type.desc then
+  if (Some "thm") = Ocaml_typing.get_simple_type (get_desc vd.Types.val_type) then
     (lid_cons lidopt s)::acc else acc

 let it_mod_1 lidopt s p md acc = (lid_cons lidopt s)::acc

 let enum0 lidopt =
-  let vl = Env.fold_values (it_val_1 lidopt) lidopt !Toploop.toplevel_env [] in
-  let ml = Env.fold_modules (it_mod_1 lidopt) lidopt !Toploop.toplevel_env [] in
-  (vl, ml)
+  try
+    let vl = Env.fold_values (it_val_1 lidopt) lidopt !Toploop.toplevel_env [] in
+    let ml = Env.fold_modules (it_mod_1 lidopt) lidopt !Toploop.toplevel_env [] in
+    (vl, ml)
+  with Not_found ->
+    (* Looking for (Longident.Lident "Stream") raises Not_found.
+       Stream is a deprecated alias module of "Stdlib.Stream", and the camlp-streams
+       package that is used by pa_hol_syntax redefines Stream, which seems to
+       confuse Env.fold_values and Env.fold_modules. *)
+    ([], [])

 let rec enum1 lidopt acc =
   match enum0 lidopt with

I checked that the updated update_database.ml works well by testing with the search commands that are exhibited at the manual from help "search".

Note that this work is orthogonal with #77.

Also minor cleanups in Makefile is done to avoid linearly increasing indentation in the if-else-fi blocks.

jrh13 / hol-light

Fix a crash in loading update_database.ml #78