src/Pure/Isar/class_declaration.ML
changeset 56921 5bf71b4da706
parent 54883 dd04a8b654fc
child 57181 2d13bf9ea77b
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Fri May 09 08:13:26 2014 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Fri May 09 08:13:28 2014 +0200
     1.3 @@ -309,11 +309,12 @@
     1.4  fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
     1.5    let
     1.6      val class = Sign.full_name thy b;
     1.7 +    val prefix = Binding.qualify true "class";
     1.8      val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
     1.9        prep_class_spec thy raw_supclasses raw_elems;
    1.10    in
    1.11      thy
    1.12 -    |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems
    1.13 +    |> Expression.add_locale I b (prefix b) supexpr elems
    1.14      |> snd |> Local_Theory.exit_global
    1.15      |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
    1.16      |-> (fn (param_map, params, assm_axiom) =>
    1.17 @@ -321,7 +322,9 @@
    1.18      #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
    1.19         Context.theory_map (Locale.add_registration (class, base_morph)
    1.20           (Option.map (rpair true) eq_morph) export_morph)
    1.21 -    #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class))
    1.22 +    #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
    1.23 +    #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
    1.24 +    |> snd
    1.25      |> Named_Target.init before_exit class
    1.26      |> pair class
    1.27    end;