# HG changeset patch
# User wenzelm
# Date 1407927146 -7200
# Node ID a3360da1d2f0c274130673052c94c954fda81aa1
# Parent  cdae2467311d8c187a324c09444ad54ab6c1dd9f
tuned whitespace;

diff -r cdae2467311d -r a3360da1d2f0 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 10:46:14 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:52:26 2014 +0200
@@ -162,14 +162,13 @@
 (* brittle context -- implicit for nested structures *)
 
 fun mark_brittle lthy =
-  if level lthy = 1
-  then map_bottom (fn (naming, operations, after_close, brittle, target) =>
-    (naming, operations, after_close, true, target)) lthy
+  if level lthy = 1 then
+    map_bottom (fn (naming, operations, after_close, brittle, target) =>
+      (naming, operations, after_close, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
-  if #brittle (top_of lthy)
-  then error "Brittle local theory context"
+  if #brittle (top_of lthy) then error "Brittle local theory context"
   else lthy;