# HG changeset patch
# User wenzelm
# Date 1221759589 -7200
# Node ID cad470c699355f9b533e8ef9d7eadb95a1d6db8a
# Parent  c49b328d689dcc57ffb68d9f502560f6c858d78f
begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};

diff -r c49b328d689d -r cad470c69935 src/Pure/Thy/thy_info.ML
--- 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 =