Remove mutability from theorem proof field

src/boss/prove_base_assumsScript.sml

@@ -123,7 +123,7 @@ val (reader:reader) = {
 
 val base_thms = read_article "base-theorems.art" reader;
 
-val _ = Net.itnet (fn th => (Thm.delete_proof th; K ())) base_thms ();
+val _ = Net.itnet Thm.delete_proof base_thms ();
 
 fun itpred P th acc = if P th then th::acc else acc;
 fun amatch tm = Net.itnet (itpred (DB.matches tm)) base_thms [];

src/opentheory/postbool/Logging.sml

@@ -708,7 +708,7 @@ fun export_thm th = let
       val _ = log_command "thm"
       val _ = if v then HOL_MESG("Finish logging\n"^(Susp.force s)^"\n") else ()
       in () end
-    val _ = delete_proof th
+    val th = delete_proof th
 in th end
 
 fun mk_path name = OS.Path.concat(OS.FileSys.getDir(),OS.Path.joinBaseExt{base=name,ext=SOME"art"})
@@ -717,8 +717,8 @@ fun mkpair f x = (f,x)
 
 datatype OTDirective = DeleteConstant | DeleteType | SkipThm | DeleteProof
 
-fun log_some_thms axdefs th =
-  (if (case Thm.proof th of
+fun log_some_thms axdefs th = let
+  val th = if (case Thm.proof th of
          Thm.Def_const_prf (thyrec, _) =>
            Lib.mem (DeleteConstant, #Name thyrec) axdefs
        | Thm.Def_const_list_prf (_,stys,_) =>
@@ -730,9 +730,9 @@ fun log_some_thms axdefs th =
        | Thm.Def_tyop_prf (thyrec,_,_,_) =>
            Lib.mem (DeleteType, #Tyop thyrec) axdefs
        | _ => false)
-   then Thm.delete_proof th
-   else ();
-   definitions := th::(!definitions))
+  then Thm.delete_proof th
+  else th;
+in definitions := th::(!definitions) end
 
 fun raw_start_logging axdefs out =
   case !log_state of

src/opentheory/postbool/loggingHolKernel.sml

@@ -23,10 +23,10 @@ struct
     val directives = Logging.read_otdfile (current_theory() ^ ".otd")
                                           handle IO.Io _ => []
     fun prepare (nm, th) =
-      (if Lib.mem (DeleteProof, nm) directives
-       then Thm.delete_proof th else ();
-       if Lib.mem (SkipThm, nm) directives
-       then NONE else SOME th)
+      (if Lib.mem (SkipThm, nm) directives then NONE
+       else SOME
+        (if Lib.mem (DeleteProof, nm) directives
+         then Thm.delete_proof th else th))
     val defs' = List.mapPartial prepare (current_definitions())
     val ths' = List.mapPartial prepare (current_theorems())
     val axs' = List.mapPartial prepare (current_axioms())

src/real/prove_real_assumsScript.sml

@@ -200,7 +200,7 @@ in
 end
 
 val base_thms = read_article "base-theorems.art" reader;
-val _ = Net.itnet (fn th => (Thm.delete_proof th; K ())) base_thms ();
+val _ = Net.itnet Thm.delete_proof base_thms ();
 
 fun itpred P th acc = if P th then th::acc else acc;
 fun amatch tm = Net.itnet (itpred (DB.matches tm)) base_thms [];
@@ -400,8 +400,8 @@ val th12 = store_thm
 
 (*
 val (pow0,powsuc) = CONJ_PAIR realaxTheory.real_pow;
-val () = Thm.delete_proof pow0
-val () = Thm.delete_proof powsuc
+val pow0 = Thm.delete_proof pow0
+val powsuc = Thm.delete_proof powsuc
  *)
 val pow0   = hd(amatch “x pow 0 = 1”);
 val powsuc = hd(amatch “x pow SUC n = x * x pow n”);

src/thm/otknl-thm.ML

@@ -107,7 +107,7 @@ end;
  * The type of theorems and some basic operations on it.                     *
  *---------------------------------------------------------------------------*)
 
-datatype thm = THM of Tag.tag * term HOLset.set * term * proof ref
+datatype thm = THM of Tag.tag * term HOLset.set * term * proof
 and proof =
   Axiom_prf
 | ASSUME_prf of term
@@ -152,8 +152,8 @@ and proof =
 | Def_spec_prf of term list * thm
 | deductAntisym_prf of thm * thm
 
-fun proof (THM(_,_,_,p)) = !p
-fun delete_proof (THM(_,_,_,p)) = p := Axiom_prf
+fun proof (THM(_,_,_,p)) = p
+fun delete_proof (THM(x,y,z,p)) = THM(x,y,z,Axiom_prf)
 
 fun single_hyp tm = HOLset.singleton Term.compare tm
 val empty_hyp = Term.empty_tmset
@@ -167,7 +167,7 @@ val hyp = hyplist   (* backwards compatibility *)
 
 fun dest_thm(t as THM(_,asl,w,_)) = (hyplist t,w) (* Compatible with old code. *)
 fun sdest_thm(THM(_,asl,w,_)) = (asl,w)
-fun make_thm R (x,y,z,p) = (Count.inc_count R; THM (x,y,z,ref p));   (* internal only *)
+fun make_thm R th = (Count.inc_count R; THM th);   (* internal only *)
 
 fun thm_frees (t as THM(_,asl,c,_)) = free_varsl (c::hyplist t);
 

src/thm/otknl-thmsig.ML

@@ -47,7 +47,7 @@ sig
   | deductAntisym_prf of thm * thm
 
   val proof : thm -> proof
-  val delete_proof : thm -> unit
+  val delete_proof : thm -> thm
   val mk_proof_thm : proof -> term list * term -> thm
 
   val deductAntisym : thm -> thm -> thm