proper theory naming after join (reset due to merge_data);
authorwenzelm
Thu Jul 04 14:20:47 2019 +0200 (2 weeks ago)
changeset 70362421727c19b23
parent 70361 34b271c4f400
child 70363 6d96ee03b62e
proper theory naming after join (reset due to merge_data);
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Thu Jul 04 12:31:24 2019 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Jul 04 14:20:47 2019 +0200
     1.3 @@ -171,7 +171,9 @@
     1.4  
     1.5  (* join theory *)
     1.6  
     1.7 -val join_theory = foldl1 Context.join_thys;
     1.8 +fun join_theory [] = raise List.Empty
     1.9 +  | join_theory [thy] = thy
    1.10 +  | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys);
    1.11  
    1.12  
    1.13  (* begin/end theory *)