finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
authorwenzelm
Sat Dec 06 00:08:07 2008 +0100 (2008-12-06)
changeset 29001b97a3f808133
parent 29000 5e03bc760355
child 29002 c9cdb569487a
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Sat Dec 06 00:04:44 2008 +0100
     1.2 +++ b/src/Pure/context.ML	Sat Dec 06 00:08:07 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/context.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7  
     1.8  Generic theory contexts with unique identity, arbitrarily typed data,
     1.9 @@ -392,14 +391,11 @@
    1.10  
    1.11  fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
    1.12    let
    1.13 -    val {name, version, intermediates} = history_of thy;
    1.14 -    val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
    1.15 -    val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
    1.16 -    val identity' = make_identity self id ids Inttab.empty;
    1.17 +    val {name, ...} = history_of thy;
    1.18 +    val Theory (identity', data', ancestry', _) = name_thy name thy;
    1.19      val history' = make_history name 0 [];
    1.20 -    val thy'' = vitalize (Theory (identity', data', ancestry', history'));
    1.21 -    val _ = List.app (fn r => r := thy'') rs;
    1.22 -  in thy'' end);
    1.23 +    val thy' = vitalize (Theory (identity', data', ancestry', history'));
    1.24 +  in thy' end);
    1.25  
    1.26  
    1.27  (* theory data *)