Fix regression by hiding "hide"; this now parses to a variable again

Also add entry-point to make the un-ignore functionality slightly
easier to get at.

src/marker/markerLib.sig

@@ -81,7 +81,9 @@ sig
   val mk_hide : string -> term -> term
   val is_hide : term -> bool
   val dest_hide : term -> string * term
-  val install_hidepp : unit -> unit
+  val install_hidepp : unit -> unit (* it starts installed *)
+  val remove_hidepp : unit -> unit
+  val unignoring_hide : ('a -> 'b) -> ('a -> 'b)
 
   val MK_HIDE : string -> thm -> thm
   val UNHIDE : thm -> thm

src/marker/markerLib.sml

@@ -516,6 +516,9 @@ fun hide_pp (tyg,tmg) backend printer ppfns gravs depth t =
 fun install_hidepp() =
     Parse.temp_add_user_printer ("hide-printer", list_mk_comb(hidec, [sv,tv]),
                                  hide_pp)
+val _ = install_hidepp()
+fun remove_hidepp() =
+    ignore (Parse.temp_remove_user_printer "hide-printer")
 
 fun mk_hide s t = list_mk_comb(hidec, [mk_var(s,bool), t])
 fun MK_HIDE s th =
@@ -572,6 +575,6 @@ val unhide_assum = unhide_assum0 first_x_assum assume_tac
 val unhide_x_assum = unhide_assum0 first_x_assum (K all_tac)
 val use_hidden_assum = unhide_assum0 first_assum (K all_tac)
 
-
+fun unignoring_hide f x = unignoringc hidec f x
 
 end

src/marker/markerScript.sml

@@ -185,5 +185,6 @@ val hideCONG = store_thm(
   REWRITE_TAC[]);
 
 val _ = Tactic.export_ignore {Name = "hide", Thy = "marker"}
+val _ = permahide “hide”
 
 val _ = export_theory();

src/marker/selftest.sml

@@ -55,6 +55,7 @@ val _ = require_msg
 val _ = new_type ("tyop", 0);
 val _ = new_constant("c1", “:tyop”)
 val _ = new_constant("c2", “:tyop”)
+val _ = overload_on ("hide", “marker$hide”);
 val asl0 = [“hide foo (P c1 /\ T /\ P x)”,
             “R c1 /\ T /\ R x”]
 val _ = tprint "RULE_ASSUM_TAC doesn't hit hide"
@@ -92,7 +93,7 @@ val _ = require_msg
                                      “R c1 /\ R x”],
                                     “Q c1 c2:bool”)]))
           (trace ("types", 1) goalprint)
-          (testtac (unignoringc “hide” (RULE_ASSUM_TAC (REWRITE_RULE[]))))
+          (testtac $ unignoring_hide $ RULE_ASSUM_TAC $ REWRITE_RULE[])
           (asl0, “Q c1 c2:bool”)
 
 val _ = new_constant("TEST", “:tyop -> bool”)