--- a/src/HOL/Proofs/Extraction/ROOT.ML Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Proofs/Extraction/ROOT.ML Wed Dec 29 17:34:41 2010 +0100
@@ -1,6 +1,12 @@
(* Examples for program extraction in Higher-Order Logic *)
-no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/Primes"];
+no_document use_thys [
+ "~~/src/HOL/Library/Efficient_Nat",
+ "~~/src/HOL/Library/Monad_Syntax",
+ "~~/src/HOL/Number_Theory/Primes"
+];
+
share_common_data ();
+
no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];