src/Pure/section_utils.ML
changeset 654 65435e2c6512
parent 613 f9eb0f819642
child 1390 bf523422a3df
     1.1 --- a/src/Pure/section_utils.ML	Mon Oct 24 10:34:28 1994 +0100
     1.2 +++ b/src/Pure/section_utils.ML	Tue Oct 25 13:13:52 1994 +0100
     1.3 @@ -61,3 +61,9 @@
     1.4  
     1.5  (*Remove the first and last charaters -- presumed to be quotes*)
     1.6  val trim = implode o escape o rev o tl o rev o tl o explode;
     1.7 +
     1.8 +
     1.9 +(*Check for some named theory*)
    1.10 +fun require_thy thy name sect =
    1.11 +  if exists (equal name o !) (stamps_of_thy thy) then ()
    1.12 +  else error ("Need at least theory " ^ quote name ^ " for " ^ sect);