tuned whitespace;
authorwenzelm
Wed Aug 13 12:52:26 2014 +0200 (2014-08-13)
changeset 57924a3360da1d2f0
parent 57923 cdae2467311d
child 57925 2bd92d3f92d7
tuned whitespace;
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 10:46:14 2014 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:52:26 2014 +0200
     1.3 @@ -162,14 +162,13 @@
     1.4  (* brittle context -- implicit for nested structures *)
     1.5  
     1.6  fun mark_brittle lthy =
     1.7 -  if level lthy = 1
     1.8 -  then map_bottom (fn (naming, operations, after_close, brittle, target) =>
     1.9 -    (naming, operations, after_close, true, target)) lthy
    1.10 +  if level lthy = 1 then
    1.11 +    map_bottom (fn (naming, operations, after_close, brittle, target) =>
    1.12 +      (naming, operations, after_close, true, target)) lthy
    1.13    else lthy;
    1.14  
    1.15  fun assert_nonbrittle lthy =
    1.16 -  if #brittle (top_of lthy)
    1.17 -  then error "Brittle local theory context"
    1.18 +  if #brittle (top_of lthy) then error "Brittle local theory context"
    1.19    else lthy;
    1.20  
    1.21