requires: check ancestors directly;
authorwenzelm
Sat Dec 13 15:00:40 2008 +0100 (2008-12-13)
changeset 29092466a83cb6f5f
parent 29091 b81fe045e799
child 29093 1cc36c0ec9eb
requires: check ancestors directly;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Sat Dec 13 15:00:39 2008 +0100
     1.2 +++ b/src/Pure/theory.ML	Sat Dec 13 15:00:40 2008 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  val copy = Context.copy_thy;
     1.5  
     1.6  fun requires thy name what =
     1.7 -  if Context.exists_name name thy then ()
     1.8 +  if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then ()
     1.9    else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
    1.10  
    1.11