# HG changeset patch
# User wenzelm
# Date 927279503 -7200
# Node ID 0c6c668c685f6770737ad27069bf1229ad731342
# Parent  08a084c79d8bf91c5c962561143a385c629d0456
backup replaced by checkpoint;

diff -r 08a084c79d8b -r 0c6c668c685f src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri May 21 11:37:36 1999 +0200
+++ b/src/Pure/pure_thy.ML	Fri May 21 11:38:23 1999 +0200
@@ -48,7 +48,7 @@
   val local_path: theory -> theory
   val begin_theory: string -> theory list -> theory
   val end_theory: theory -> theory
-  val backup: theory -> theory
+  val checkpoint: theory -> theory
   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
   val dummy_patternN: string
 end;
@@ -361,16 +361,14 @@
 
 fun end_theory thy = Theory.add_name (get_name thy) thy;
 
-
-(* make backup copy *)
-
-fun backup thy =
-  let val {name, version} = get_info thy in
-    thy
-    |> Theory.prep_ext
-    |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int version)
-    |> put_info {name = name, version = version + 1}
-  end;
+fun checkpoint thy =
+  if is_draft thy then
+    let val {name, version} = get_info thy in
+      thy
+      |> Theory.add_name (name ^ ":" ^ string_of_int version)
+      |> put_info {name = name, version = version + 1}
+    end
+  else thy;