src/HOL/Extraction/ROOT.ML

--- a/src/HOL/Extraction/ROOT.ML	Sat Nov 10 14:31:23 2007 +0100
+++ b/src/HOL/Extraction/ROOT.ML	Sat Nov 10 14:36:33 2007 +0100
@@ -7,6 +7,6 @@
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running extraction examples"
 else
-  (proofs := 2;
+  (Proofterm.proofs := 2;
    no_document time_use_thy "Efficient_Nat";
    use_thys ["QuotRem", "Warshall", "Higman", "Pigeonhole"]);