src/Pure/Isar/class.ML
changeset 25268 58146cb7bf44
parent 25239 3d6abdd10382
child 25311 aa750e3a581c
     1.1 --- a/src/Pure/Isar/class.ML	Fri Nov 02 18:52:58 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Nov 02 18:52:59 2007 +0100
     1.3 @@ -537,9 +537,7 @@
     1.4      val class_intros = these_intros thy;
     1.5      val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
     1.6    in
     1.7 -    (ALLGOALS (Method.insert_tac facts THEN'
     1.8 -      REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros)))
     1.9 -    THEN Tactic.distinct_subgoals_tac) st
    1.10 +    Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st
    1.11    end;
    1.12  
    1.13  fun default_intro_classes_tac [] = intro_classes_tac []
    1.14 @@ -596,8 +594,9 @@
    1.15  
    1.16  fun prove_subclass (sub, sup) thms ctxt thy =
    1.17    let
    1.18 -    val supclasses = Sign.complete_sort thy [sup]
    1.19 -      |> filter_out (fn class => Sign.subsort thy ([sub], [class]));
    1.20 +    val classes = ClassData.get thy;
    1.21 +    val is_sup = not o null o curry (Graph.irreducible_paths classes) sub;
    1.22 +    val supclasses = Graph.all_succs classes [sup] |> filter_out is_sup;
    1.23      fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
    1.24    in
    1.25      thy
    1.26 @@ -844,6 +843,7 @@
    1.27                calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
    1.28        #> class_interpretation class axioms []
    1.29        )))))
    1.30 +    |> init class
    1.31      |> pair class
    1.32    end;
    1.33