author | wenzelm |
Thu, 04 Jul 2019 14:20:47 +0200 | |
changeset 70362 | 421727c19b23 |
parent 70361 | 34b271c4f400 |
child 70363 | 6d96ee03b62e |
--- a/src/Pure/theory.ML Thu Jul 04 12:31:24 2019 +0200 +++ b/src/Pure/theory.ML Thu Jul 04 14:20:47 2019 +0200 @@ -171,7 +171,9 @@ (* join theory *) -val join_theory = foldl1 Context.join_thys; +fun join_theory [] = raise List.Empty + | join_theory [thy] = thy + | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys); (* begin/end theory *)