| changeset 29092 | 466a83cb6f5f |
| parent 29004 | a5a91f387791 |
| child 29581 | b3b33e0298eb |
--- 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);