diff -r ba5be5c3d477 -r aa533c5e3f48 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Nov 28 14:01:20 2010 +0100
+++ b/src/Pure/Isar/overloading.ML	Sun Nov 28 15:28:48 2010 +0100
@@ -48,15 +48,16 @@
 );
 
 fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
-  secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => let
+    secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } =>
+  let
     val (((primary_constraints', secondary_constraints'),
       (((improve', subst'), consider_abbrevs'), unchecks')), passed')
         = f (((primary_constraints, secondary_constraints),
             (((improve, subst), consider_abbrevs), unchecks)), passed)
   in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
     improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
-    unchecks = unchecks', passed = passed'
-  } end);
+    unchecks = unchecks', passed = passed' }
+  end);
 
 val mark_passed = (map_improvable_syntax o apsnd) (K true);
 
@@ -80,7 +81,8 @@
           | NONE => NONE)
         | _ => NONE) t;
     val ts'' = if is_abbrev then ts' else map apply_subst ts';
-  in if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
+  in
+    if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
     if passed_or_abbrev then SOME (ts'', ctxt)
     else SOME (ts'', ctxt
       |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
@@ -166,9 +168,11 @@
 fun conclude lthy =
   let
     val overloading = get_overloading lthy;
-    val _ = if null overloading then () else
-      error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
-        o Syntax.string_of_term lthy o Const o fst) overloading));
+    val _ =
+      if null overloading then ()
+      else
+        error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
+          o Syntax.string_of_term lthy o Const o fst) overloading));
   in lthy end;
 
 fun gen_overloading prep_const raw_overloading thy =