src/Pure/Isar/class_declaration.ML
changeset 51685 385ef6706252
parent 51551 88d1d19fb74f
child 52636 238cec044ebf
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Apr 10 13:10:38 2013 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Apr 10 15:30:19 2013 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
     1.5      val sup_of_classes = map (snd o Class.rules thy) sups;
     1.6      val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
     1.7 -    val axclass_intro = #intro (AxClass.get_info thy class);
     1.8 +    val axclass_intro = #intro (Axclass.get_info thy class);
     1.9      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
    1.10      val tac =
    1.11        REPEAT (SOMEGOAL
    1.12 @@ -289,13 +289,13 @@
    1.13        |> fst
    1.14        |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
    1.15      fun get_axiom thy =
    1.16 -      (case #axioms (AxClass.get_info thy class) of
    1.17 +      (case #axioms (Axclass.get_info thy class) of
    1.18           [] => NONE
    1.19        | [thm] => SOME thm);
    1.20    in
    1.21      thy
    1.22      |> add_consts class base_sort sups supparam_names global_syntax
    1.23 -    |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
    1.24 +    |-> (fn (param_map, params) => Axclass.define_class (bname, supsort)
    1.25            (map (fst o snd) params)
    1.26            [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
    1.27      #> snd
    1.28 @@ -346,7 +346,7 @@
    1.29        (case Named_Target.peek lthy of
    1.30           SOME {target, is_class = true, ...} => target
    1.31        | _ => error "Not in a class target");
    1.32 -    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
    1.33 +    val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
    1.34  
    1.35      val expr = ([(sup, (("", false), Expression.Positional []))], []);
    1.36      val (([props], deps, export), goal_ctxt) =