# HG changeset patch
# User wenzelm
# Date 1290197652 -3600
# Node ID 2d9222a2239d429bafc3050db6a2942965401bcf
# Parent  2df58ba31be7cfbd855b87a5ab62b51b98e96c99
do not export Thy_Load.required, to avoid confusion about the interface;

diff -r 2df58ba31be7 -r 2d9222a2239d src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Nov 19 09:07:23 2010 -0800
+++ b/src/Pure/Thy/thy_load.ML	Fri Nov 19 21:14:12 2010 +0100
@@ -20,7 +20,6 @@
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
-  val require: Path.T -> theory -> theory
   val provide: Path.T * (Path.T * File.ident) -> theory -> theory
   val check_file: Path.T list -> Path.T -> Path.T * File.ident
   val check_thy: Path.T -> string -> Path.T * File.ident