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);