tuned;

--- a/src/Pure/Isar/class_declaration.ML	Thu Jun 09 12:02:38 2016 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Thu Jun 09 12:16:52 2016 +0200
@@ -348,9 +348,10 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
-    val proto_sub = case Named_Target.class_of lthy of
+    val proto_sub =
+      (case Named_Target.class_of lthy of
         SOME class => class
-      | NONE => error "Not in a class target";
+      | NONE => error "Not in a class target");
     val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
 
     val expr = ([(sup, (("", false), Expression.Positional []))], []);

--- a/src/Pure/Isar/named_target.ML	Thu Jun 09 12:02:38 2016 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Jun 09 12:16:52 2016 +0200
@@ -40,14 +40,14 @@
   else NONE;
 
 fun is_theory lthy =
-  case get_data lthy of
+  (case get_data lthy of
     SOME ("", _) => true
-  | _ => false;
+  | _ => false);
 
 fun target_of lthy =
-  case get_data lthy of
+  (case get_data lthy of
     NONE => error "Not in a named target"
-  | SOME (target, _) => target;
+  | SOME (target, _) => target);
 
 fun locale_name_of NONE = NONE
   | locale_name_of (SOME ("", _)) = NONE
@@ -58,9 +58,9 @@
 val bottom_locale_of = locale_name_of o get_bottom_data;
 
 fun class_of lthy =
-  case get_data lthy of
+  (case get_data lthy of
     SOME (class, true) => SOME class
-  | _ => NONE;
+  | _ => NONE);
 
 
 (* operations *)