changeset 17756 | d4a35f82fbb4 |
parent 17365 | a8e19032497d |
child 18678 | dd0c569fa43d |
--- a/src/Pure/Thy/thy_info.ML Tue Oct 04 16:47:40 2005 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Oct 04 19:01:37 2005 +0200 @@ -364,7 +364,7 @@ val thy = if not really then SOME (get_theory name) else NONE; val result = - if current andalso forall #1 parent_results then true + if current andalso forall fst parent_results then true else ((case new_deps of SOME deps => change_thys (update_node name (map base_of_path parents) (deps, thy))