proper theory naming after join (reset due to merge_data);
authorwenzelm
Thu, 04 Jul 2019 14:20:47 +0200
changeset 70362 421727c19b23
parent 70361 34b271c4f400
child 70363 6d96ee03b62e
proper theory naming after join (reset due to merge_data);
src/Pure/theory.ML
--- 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 *)