src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Tue Jan 08 12:39:39 2013 +0100
+++ b/src/Pure/axclass.ML	Tue Jan 08 12:50:57 2013 +0100
@@ -187,11 +187,7 @@
   let
     fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) =
       let
-        val proven = is_classrel thy1;
-        val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
-        val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
-
-        fun complete c1 c2 (finished2, thy2) =
+        fun compl c1 c2 (finished2, thy2) =
           if is_classrel thy2 (c1, c2) then (finished2, thy2)
           else
             (false,
@@ -200,12 +196,17 @@
                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
                 |> Drule.instantiate' [SOME (ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
                 |> Thm.close_derivation));
-      in fold_product complete preds succs (finished1, thy1) end;
 
-    val (finished', thy') =
-      Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy);
+        val proven = is_classrel thy1;
+        val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
+        val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
+      in
+        fold_product compl preds succs (finished1, thy1)
+      end;
   in
-    if finished' then NONE else SOME thy'
+    (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of
+      (true, _) => NONE
+    | (_, thy') => SOME thy')
   end;
 
 
@@ -256,7 +257,8 @@
   let
     val arities = proven_arities_of thy;
     val (finished, arities') =
-      Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars) arities (true, arities);
+      Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars)
+        arities (true, arities);
   in
     if finished then NONE
     else SOME (map_proven_arities (K arities') thy)
@@ -387,8 +389,9 @@
     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
-    val (th', thy') = Global_Theory.store_thm
-      (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
+    val (th', thy') =
+      Global_Theory.store_thm
+        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
     val th'' = th'
       |> Thm.unconstrainT
       |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
@@ -407,8 +410,9 @@
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
 
-    val (th', thy') = Global_Theory.store_thm
-      (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
+    val (th', thy') =
+      Global_Theory.store_thm
+        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
 
     val args = Name.invent_names Name.context Name.aT Ss;
     val T = Type (t, map TFree args);