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