# HG changeset patch
# User wenzelm
# Date 1194701793 -3600
# Node ID 7657a081fcb4c65aaf375d18cfcdadde5e6a604d
# Parent  ccbf65080fdf0844b7db8213bddeb5551d7f8065
qualified Proofterm.proofs;

diff -r ccbf65080fdf -r 7657a081fcb4 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"]);
diff -r ccbf65080fdf -r 7657a081fcb4 src/HOL/Import/ROOT.ML
--- a/src/HOL/Import/ROOT.ML	Sat Nov 10 14:31:23 2007 +0100
+++ b/src/HOL/Import/ROOT.ML	Sat Nov 10 14:36:33 2007 +0100
@@ -3,6 +3,6 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-proofs := 0;
+Proofterm.proofs := 0;
 use_thy "HOL4Compat";
 use_thy "HOL4Syntax";
diff -r ccbf65080fdf -r 7657a081fcb4 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Sat Nov 10 14:31:23 2007 +0100
+++ b/src/HOL/Lambda/ROOT.ML	Sat Nov 10 14:36:33 2007 +0100
@@ -5,7 +5,7 @@
 *)
 
 Syntax.ambiguity_level := 100;
-proofs := 2;
+Proofterm.proofs := 2;
 
 no_document use_thys ["Accessible_Part", "Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization"];
diff -r ccbf65080fdf -r 7657a081fcb4 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Sat Nov 10 14:31:23 2007 +0100
+++ b/src/HOL/ex/ROOT.ML	Sat Nov 10 14:36:33 2007 +0100
@@ -56,7 +56,7 @@
   "Adder"
 ];
 
-setmp proofs 2 time_use_thy "Hilbert_Classical";
+setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
 
 time_use_thy "Classical";
 time_use_thy "set";