# HG changeset patch
# User wenzelm
# Date 783087232 -3600
# Node ID 65435e2c6512676363824e16934d49f007fe26e8
# Parent  6eeff82979df5ec5227538a6b1bb0b45b1172dbb
added require_thy;

diff -r 6eeff82979df -r 65435e2c6512 src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Mon Oct 24 10:34:28 1994 +0100
+++ b/src/Pure/section_utils.ML	Tue Oct 25 13:13:52 1994 +0100
@@ -61,3 +61,9 @@
 
 (*Remove the first and last charaters -- presumed to be quotes*)
 val trim = implode o escape o rev o tl o rev o tl o explode;
+
+
+(*Check for some named theory*)
+fun require_thy thy name sect =
+  if exists (equal name o !) (stamps_of_thy thy) then ()
+  else error ("Need at least theory " ^ quote name ^ " for " ^ sect);