tuned;

--- a/src/Pure/Isar/class_declaration.ML	Sat Mar 10 16:49:34 2012 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sat Mar 10 17:07:10 2012 +0100
@@ -74,13 +74,12 @@
         val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
         val const_eq_morph =
           (case eq_morph of
-             SOME eq_morph => const_morph $> eq_morph
+            SOME eq_morph => const_morph $> eq_morph
           | NONE => const_morph);
         val thm'' = Morphism.thm const_eq_morph thm';
         val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
       in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
-    val assm_intro = Option.map prove_assm_intro
-      (fst (Locale.intros_of thy class));
+    val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
 
     (* of_class *)
     val of_class_prop_concl = Logic.mk_of_class (aT, class);

--- a/src/Pure/Isar/element.ML	Sat Mar 10 16:49:34 2012 +0100
+++ b/src/Pure/Isar/element.ML	Sat Mar 10 17:07:10 2012 +0100
@@ -461,11 +461,13 @@
 
 (* rewriting with equalities *)
 
-fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
- {binding = [],
-  typ = [],
-  term = [Raw_Simplifier.rewrite_term thy thms []],
-  fact = [map (Raw_Simplifier.rewrite_rule thms)]});
+fun eq_morphism _ [] = NONE
+  | eq_morphism thy thms =
+      SOME (Morphism.morphism
+       {binding = [],
+        typ = [],
+        term = [Raw_Simplifier.rewrite_term thy thms []],
+        fact = [map (Raw_Simplifier.rewrite_rule thms)]});
 
 
 (* transfer to theory using closure *)

--- a/src/Pure/Isar/expression.ML	Sat Mar 10 16:49:34 2012 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 10 17:07:10 2012 +0100
@@ -899,8 +899,7 @@
     |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
       fn thy =>
         Locale.add_dependency target
-          (dep, morph $> Element.satisfy_morphism
-            (map (Element.transform_witness export') wits))
+          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
           (Element.eq_morphism thy eqns' |> Option.map (rpair true))
           export thy) (deps ~~ witss))
   end;