# HG changeset patch
# User wenzelm
# Date 1248791329 -7200
# Node ID 8b02619c3039384bb6b049bdcf675d1f65e873cd
# Parent  d9def420c84e695c20558ebf5809a01fb2c608f5
non-critical use_thy;

diff -r d9def420c84e -r 8b02619c3039 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Jul 28 15:10:15 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Jul 28 16:28:49 2009 +0200
@@ -68,7 +68,7 @@
   "Landau"
 ];
 
-setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
+setmp_noncritical proofs 2 use_thy "Hilbert_Classical";
 
 
 use_thy "SVC_Oracle";