src/HOL/Import/replay.ML
changeset 32966 5b21661fe618
parent 32960 69916a850301
child 32970 fbd2bb2489a8
     1.1 --- a/src/HOL/Import/replay.ML	Sat Oct 17 15:55:57 2009 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Sat Oct 17 15:57:51 2009 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4  
     1.5  fun replay_chached_thm int_thms thyname thmname =
     1.6      let
     1.7 -        fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
     1.8 +        fun th_of thy = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
     1.9          fun err msg = raise ERR "replay_cached_thm" msg
    1.10          val _ = writeln ("Replaying (from cache) "^thmname^" ...")
    1.11          fun rps [] thy = thy