src/Pure/Isar/class.ML
changeset 24930 cc2e0e8c81af
parent 24920 2a45e400fdad
child 24949 5f00e3532418
     1.1 --- a/src/Pure/Isar/class.ML	Tue Oct 09 17:10:41 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Oct 09 17:10:43 2007 +0200
     1.3 @@ -379,7 +379,7 @@
     1.4    let
     1.5      fun params class =
     1.6        let
     1.7 -        val const_typs = (#params o AxClass.get_definition thy) class;
     1.8 +        val const_typs = (#params o AxClass.get_info thy) class;
     1.9          val const_names = (#consts o the_class_data thy) class;
    1.10        in
    1.11          (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
    1.12 @@ -434,7 +434,7 @@
    1.13          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
    1.14        Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
    1.15        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
    1.16 -        o these o Option.map #params o try (AxClass.get_definition thy)) class,
    1.17 +        o these o Option.map #params o try (AxClass.get_info thy)) class,
    1.18        (SOME o Pretty.block o Pretty.breaks) [
    1.19          Pretty.str "instances:",
    1.20          Pretty.list "" "" (map (mk_arity class) (the_arities class))
    1.21 @@ -474,7 +474,7 @@
    1.22  fun class_intro thy locale class sups =
    1.23    let
    1.24      fun class_elim class =
    1.25 -      case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
    1.26 +      case (map Drule.unconstrainTs o #axioms o AxClass.get_info thy) class
    1.27         of [thm] => SOME thm
    1.28          | [] => NONE;
    1.29      val pred_intro = case Locale.intros thy locale
    1.30 @@ -484,7 +484,7 @@
    1.31        | _ => NONE;
    1.32      val pred_intro' = pred_intro
    1.33        |> Option.map (fn intro => intro OF map_filter class_elim sups);
    1.34 -    val class_intro = (#intro o AxClass.get_definition thy) class;
    1.35 +    val class_intro = (#intro o AxClass.get_info thy) class;
    1.36      val raw_intro = case pred_intro'
    1.37       of SOME pred_intro => class_intro |> OF_LAST pred_intro
    1.38        | NONE => class_intro;
    1.39 @@ -534,18 +534,15 @@
    1.40      val classes = Sign.all_classes thy;
    1.41      val class_trivs = map (Thm.class_triv thy) classes;
    1.42      val class_intros = these_intros thy;
    1.43 -    fun add_axclass_intro class =
    1.44 -      case try (AxClass.get_definition thy) class of SOME {intro, ...} => cons intro | _ => I;
    1.45 -    val axclass_intros = fold add_axclass_intro classes [];
    1.46 +    val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
    1.47    in
    1.48 -    st
    1.49 -    |> ((ALLGOALS (Method.insert_tac facts THEN'
    1.50 -          REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros))))
    1.51 -            THEN Tactic.distinct_subgoals_tac)
    1.52 +    (ALLGOALS (Method.insert_tac facts THEN'
    1.53 +      REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros)))
    1.54 +    THEN Tactic.distinct_subgoals_tac) st
    1.55    end;
    1.56  
    1.57  fun default_intro_classes_tac [] = intro_classes_tac []
    1.58 -  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
    1.59 +  | default_intro_classes_tac _ = no_tac;
    1.60  
    1.61  fun default_tac rules ctxt facts =
    1.62    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE