# HG changeset patch
# User haftmann
# Date 1399616008 -7200
# Node ID 5bf71b4da7067b8b73ba87e54fbbda8451b90e0f
# Parent  d651b944c67ee035d70959b45f98bf2927ede2f3
note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs

diff -r d651b944c67e -r 5bf71b4da706 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Fri May 09 08:13:26 2014 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Fri May 09 08:13:28 2014 +0200
@@ -309,11 +309,12 @@
 fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy b;
+    val prefix = Binding.qualify true "class";
     val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
       prep_class_spec thy raw_supclasses raw_elems;
   in
     thy
-    |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems
+    |> Expression.add_locale I b (prefix b) supexpr elems
     |> snd |> Local_Theory.exit_global
     |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     |-> (fn (param_map, params, assm_axiom) =>
@@ -321,7 +322,9 @@
     #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
        Context.theory_map (Locale.add_registration (class, base_morph)
          (Option.map (rpair true) eq_morph) export_morph)
-    #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class))
+    #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
+    #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
+    |> snd
     |> Named_Target.init before_exit class
     |> pair class
   end;