src/Pure/Isar/class.ML
changeset 31944 c8a35979a5bc
parent 31943 5e960a0780a2
child 31987 f4c7be4d684f
     1.1 --- a/src/Pure/Isar/class.ML	Mon Jul 06 19:58:52 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Jul 06 20:36:38 2009 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4      val sup_of_classes = map (snd o rules thy) sups;
     1.5      val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
     1.6      val axclass_intro = #intro (AxClass.get_info thy class);
     1.7 -    val base_sort_trivs = Thm.sort_triv thy (aT, base_sort);
     1.8 +    val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
     1.9      val tac = REPEAT (SOMEGOAL
    1.10        (Tactic.match_tac (axclass_intro :: sup_of_classes
    1.11           @ loc_axiom_intros @ base_sort_trivs)