changeset 72627 | 8d83acc5062e |
parent 72626 | 5a616815cc44 |
child 72634 | 5cea0993ee4f |
--- a/src/Pure/Thy/sessions.scala Mon Nov 16 23:19:07 2020 +0100 +++ b/src/Pure/Thy/sessions.scala Mon Nov 16 23:27:43 2020 +0100 @@ -357,7 +357,7 @@ base: Base, infos: List[Info]) { - def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) + def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors)) } def base_info(options: Options,