tuned;

--- a/src/Pure/Isar/class.ML	Wed Mar 21 23:41:22 2012 +0100
+++ b/src/Pure/Isar/class.ML	Thu Mar 22 10:10:30 2012 +0100
@@ -145,10 +145,12 @@
 fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
 
 val base_morphism = #base_morph oo the_class_data;
+
 fun morphism thy class =
   (case Element.eq_morphism thy (these_defs thy [class]) of
     SOME eq_morph => base_morphism thy class $> eq_morph
   | NONE => base_morphism thy class);
+
 val export_morphism = #export_morph oo the_class_data;
 
 fun print_classes ctxt =
@@ -228,9 +230,9 @@
     val intros = (snd o rules thy) sup :: map_filter I
       [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
         (fst o rules thy) sub];
-    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
-    val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
-      (K tac);
+    val classrel =
+      Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+        (K (EVERY (map (TRYALL o Tactic.rtac) intros)));
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
@@ -312,14 +314,14 @@
 
 val class_prefix = Logic.const_of_class o Long_Name.base_name;
 
+local
+
 fun target_extension f class lthy =
   lthy
   |> Local_Theory.raw_theory f
   |> Local_Theory.target (synchronize_class_syntax [class]
       (base_sort (Proof_Context.theory_of lthy) class));
 
-local
-
 fun target_const class ((c, mx), (type_params, dict)) thy =
   let
     val morph = morphism thy class;
@@ -478,8 +480,9 @@
 
 (* target *)
 
-fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
-    (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
+fun define_overloaded (c, U) v (b_def, rhs) =
+  Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
+  ##>> AxClass.define_overloaded b_def (c, rhs))
   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_inst_syntax;
 
@@ -603,8 +606,8 @@
     val (tycos, vs, sort) = read_multi_arity thy raw_arities;
     val sorts = map snd vs;
     val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
-    fun after_qed results = Proof_Context.background_theory
-      ((fold o fold) AxClass.add_arity results);
+    fun after_qed results =
+      Proof_Context.background_theory ((fold o fold) AxClass.add_arity results);
   in
     thy
     |> Proof_Context.init_global