equal
deleted
inserted
replaced
66 |
66 |
67 val checkpoint = Context.checkpoint_thy; |
67 val checkpoint = Context.checkpoint_thy; |
68 val copy = Context.copy_thy; |
68 val copy = Context.copy_thy; |
69 |
69 |
70 fun requires thy name what = |
70 fun requires thy name what = |
71 if Context.exists_name name thy then () |
71 if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then () |
72 else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); |
72 else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); |
73 |
73 |
74 |
74 |
75 |
75 |
76 (** datatype thy **) |
76 (** datatype thy **) |