# HG changeset patch
# User wenzelm
# Date 1376938029 -7200
# Node ID 6cd0feb85e35d0133b7392969ba3851c7fe13682
# Parent  5a1dcda7967cc1d2fb69c615609884fdba77c833
tuned;

diff -r 5a1dcda7967c -r 6cd0feb85e35 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Aug 19 20:37:36 2013 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Aug 19 20:47:09 2013 +0200
@@ -45,15 +45,16 @@
   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
     {target = target, is_locale = is_locale, is_class = is_class});
 
-fun is_theory lthy = Option.map #target (peek lthy) = SOME ""
-  andalso Local_Theory.level lthy = 1;
+fun is_theory lthy =
+  Option.map #target (peek lthy) = SOME "" andalso Local_Theory.level lthy = 1;
 
 fun the_name lthy =
   let
     val _ = Local_Theory.assert_bottom true lthy;
-  in case Option.map #target (peek lthy) of
+  in
+    (case Option.map #target (peek lthy) of
       SOME target => target
-    | _ => error "Not in a named target"
+    | _ => error "Not in a named target")
   end;