more thorough checks for theory name consistency (for extend, not just merge);
authorwenzelm
Wed May 16 15:18:12 2018 +0200 (12 months ago)
changeset 6819314dd78f036ba
parent 68192 73a1b393d6f9
child 68194 796f2585c7ee
more thorough checks for theory name consistency (for extend, not just merge);
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Tue May 15 17:07:41 2018 +0200
     1.2 +++ b/src/Pure/context.ML	Wed May 16 15:18:12 2018 +0200
     1.3 @@ -359,7 +359,7 @@
     1.4  
     1.5  val update_thy = change_thy false;
     1.6  val extend_thy = update_thy I;
     1.7 -val finish_thy = change_thy true I;
     1.8 +val finish_thy = change_thy true I #> tap extend_thy;
     1.9  
    1.10  end;
    1.11  
    1.12 @@ -399,7 +399,7 @@
    1.13  
    1.14        val history = make_history name 0;
    1.15        val ancestry = make_ancestry parents ancestors;
    1.16 -    in create_thy ids history ancestry (data_of thy0) end;
    1.17 +    in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
    1.18  
    1.19  end;
    1.20