src/Pure/theory.ML

   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val nodes_of: theory -> theory list
   val merge: theory * theory -> theory
   val merge_list: theory list -> theory
-  val requires: theory -> string -> string -> unit
   val setup: (theory -> theory) -> unit
   val get_markup: theory -> Markup.T
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
   val axioms_of: theory -> (string * term) list

 val merge = Context.merge;
 
 fun merge_list [] = raise THEORY ("Empty merge of theories", [])
   | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
 
-fun requires thy name what =
-  if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
-  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
-
 fun setup f = Context.>> (Context.map_theory f);
 
 
 
 (** datatype thy **)