src/Pure/section_utils.ML

 	   then front @ escape (tl (snd (take_prefix is_blank rest)))
 	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
 
 (*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);