# HG changeset patch
# User haftmann
# Date 1194025979 -3600
# Node ID 58146cb7bf44fb0f5961e0c3fd10eb8c75b33a94
# Parent  1f745c599b5cc1046185977cab1ac569a2f1631a
more precise treatment of prove_subclass

diff -r 1f745c599b5c -r 58146cb7bf44 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Nov 02 18:52:58 2007 +0100
+++ b/src/Pure/Isar/class.ML	Fri Nov 02 18:52:59 2007 +0100
@@ -537,9 +537,7 @@
     val class_intros = these_intros thy;
     val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   in
-    (ALLGOALS (Method.insert_tac facts THEN'
-      REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros)))
-    THEN Tactic.distinct_subgoals_tac) st
+    Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st
   end;
 
 fun default_intro_classes_tac [] = intro_classes_tac []
@@ -596,8 +594,9 @@
 
 fun prove_subclass (sub, sup) thms ctxt thy =
   let
-    val supclasses = Sign.complete_sort thy [sup]
-      |> filter_out (fn class => Sign.subsort thy ([sub], [class]));
+    val classes = ClassData.get thy;
+    val is_sup = not o null o curry (Graph.irreducible_paths classes) sub;
+    val supclasses = Graph.all_succs classes [sup] |> filter_out is_sup;
     fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
   in
     thy
@@ -844,6 +843,7 @@
               calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
       #> class_interpretation class axioms []
       )))))
+    |> init class
     |> pair class
   end;