# HG changeset patch # User wenzelm # Date 1228518487 -3600 # Node ID b97a3f80813318dcaae4d0d2671b8ae6d2bc2e8f # Parent 5e03bc7603551c88c5763211e5317392de89d31d finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs); diff -r 5e03bc760355 -r b97a3f808133 src/Pure/context.ML --- a/src/Pure/context.ML Sat Dec 06 00:04:44 2008 +0100 +++ b/src/Pure/context.ML Sat Dec 06 00:08:07 2008 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/context.ML - ID: $Id$ Author: Markus Wenzel, TU Muenchen Generic theory contexts with unique identity, arbitrarily typed data, @@ -392,14 +391,11 @@ fun finish_thy thy = NAMED_CRITICAL "theory" (fn () => let - val {name, version, intermediates} = history_of thy; - val rs = map ((fn TheoryRef r => r) o check_thy) intermediates; - val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy; - val identity' = make_identity self id ids Inttab.empty; + val {name, ...} = history_of thy; + val Theory (identity', data', ancestry', _) = name_thy name thy; val history' = make_history name 0 []; - val thy'' = vitalize (Theory (identity', data', ancestry', history')); - val _ = List.app (fn r => r := thy'') rs; - in thy'' end); + val thy' = vitalize (Theory (identity', data', ancestry', history')); + in thy' end); (* theory data *)