# HG changeset patch
# User wenzelm
# Date 1320844544 -3600
# Node ID 2bef6da4a6a66792f82e944547a60b3a632ebcc7
# Parent  d17556b9a89bb38d390e575bae21cf20104266f7
tuned layout;

diff -r d17556b9a89b -r 2bef6da4a6a6 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 11:35:09 2011 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 14:15:44 2011 +0100
@@ -104,7 +104,8 @@
     (* user space type system: only permits 'a type variable, improves towards 'a *)
     val algebra = Sign.classes_of thy;
     val inter_sort = curry (Sorts.inter_sort algebra);
-    val proto_base_sort = if null sups then Sign.defaultS thy
+    val proto_base_sort =
+      if null sups then Sign.defaultS thy
       else fold inter_sort (map (Class.base_sort thy) sups) [];
     val base_constraints = (map o apsnd)
       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
@@ -116,19 +117,19 @@
     fun singleton_fixate Ts =
       let
         fun extract f = (fold o fold_atyps) f Ts [];
-        val tfrees = extract
-          (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
-        val inferred_sort = extract
-          (fn TVar (_, sort) => inter_sort sort | _ => I);
-        val fixate_sort = if null tfrees then inferred_sort
-          else case tfrees
-           of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
+        val tfrees = extract (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
+        val inferred_sort = extract (fn TVar (_, sort) => inter_sort sort | _ => I);
+        val fixate_sort =
+          if null tfrees then inferred_sort
+          else
+            (case tfrees of
+              [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
                 then inter_sort a_sort inferred_sort
                 else error ("Type inference imposes additional sort constraint "
                   ^ Syntax.string_of_sort_global thy inferred_sort
                   ^ " of type parameter " ^ Name.aT ^ " of sort "
                   ^ Syntax.string_of_sort_global thy a_sort)
-            | _ => error "Multiple type variables in class specification";
+            | _ => error "Multiple type variables in class specification");
       in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
     fun after_infer_fixate Ts =
       let
@@ -158,18 +159,22 @@
       | filter_element (e as Element.Constrains _) = SOME e
       | filter_element (Element.Assumes []) = NONE
       | filter_element (e as Element.Assumes _) = SOME e
-      | filter_element (Element.Defines _) = error ("\"defines\" element not allowed in class specification.")
-      | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification.");
+      | filter_element (Element.Defines _) =
+          error ("\"defines\" element not allowed in class specification.")
+      | filter_element (Element.Notes _) =
+          error ("\"notes\" element not allowed in class specification.");
     val inferred_elems = map_filter filter_element raw_inferred_elems;
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
       | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
       | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
           fold_types f t #> (fold o fold_types) f ts) o snd) assms;
-    val base_sort = if null inferred_elems then proto_base_sort else
-      case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
-       of [] => error "No type variable in class specification"
+    val base_sort =
+      if null inferred_elems then proto_base_sort
+      else
+        (case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] of
+          [] => error "No type variable in class specification"
         | [(_, sort)] => sort
-        | _ => error "Multiple type variables in class specification";
+        | _ => error "Multiple type variables in class specification");
     val supparams = map (fn ((c, T), _) =>
       (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
     val supparam_names = map fst supparams;
@@ -317,6 +322,7 @@
 end; (*local*)
 
 
+
 (** subclass relations **)
 
 local