begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};

--- a/src/Pure/Thy/thy_info.ML	Thu Sep 18 19:39:47 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Sep 18 19:39:49 2008 +0200
@@ -541,7 +541,8 @@
       |> Present.begin_theory update_time dir uses;
 
     val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
-    val theory'' = fold (Context.theory_map o exec_file false) uses_now theory';
+    val theory'' =
+      fold (fn x => Context.theory_map (exec_file false x) o Theory.checkpoint) uses_now theory';
   in theory'' end;
 
 fun end_theory theory =