more standard name bindings (amending 5bf71b4da706): avoid odd full_name like "Orderings.class.Orderings.preorder.of_class.intro" with many redundant name space accesses;

--- a/NEWS	Tue May 02 14:19:34 2023 +0200
+++ b/NEWS	Tue May 02 19:49:17 2023 +0200
@@ -7,6 +7,17 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* The special "of_class" introduction rule for 'class' definitions has
+been renamed from "class.NAME.of_class.intro" to "NAME.intro_of_class"
+(where NAME is the name specification of the class). E.g. see the HOL
+library:
+
+  class.preorder.of_class.intro  ~>  preorder.intro_of_class
+  class.order.of_class.intro  ~> order.intro_of_class
+
+
 *** Document preparation ***
 
 * Various well-known LaTeX styles are included as Isabelle components,

--- a/src/HOL/Library/Lexord.thy	Tue May 02 14:19:34 2023 +0200
+++ b/src/HOL/Library/Lexord.thy	Tue May 02 19:49:17 2023 +0200
@@ -153,7 +153,7 @@
     and less_list = lex.lex_less ..
 
 instance
-  by (rule class.preorder.of_class.intro, rule preordering_preorderI, fact lex.preordering)
+  by (rule preorder.intro_of_class, rule preordering_preorderI, fact lex.preordering)
 
 end
 
@@ -171,7 +171,7 @@
 qed
 
 instance list :: (order) order
-  by (rule class.order.of_class.intro, rule ordering_orderI, fact lex.ordering)
+  by (rule order.intro_of_class, rule ordering_orderI, fact lex.ordering)
 
 export_code \<open>(\<le>) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> \<open>(<) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> in Haskell
 

--- a/src/HOL/Library/Poly_Mapping.thy	Tue May 02 14:19:34 2023 +0200
+++ b/src/HOL/Library/Poly_Mapping.thy	Tue May 02 19:49:17 2023 +0200
@@ -910,7 +910,7 @@
   is "\<lambda>f g. less_fun f g \<or> f = g"
   .
 
-instance proof (rule class.Orderings.linorder.of_class.intro)
+instance proof (rule linorder.intro_of_class)
   show "class.linorder (less_eq :: (_ \<Rightarrow>\<^sub>0 _) \<Rightarrow> _) less"
   proof (rule linorder_strictI, rule order_strictI)
     fix f g h :: "'a \<Rightarrow>\<^sub>0 'b"

--- a/src/Pure/Isar/class_declaration.ML	Tue May 02 14:19:34 2023 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue May 02 19:49:17 2023 +0200
@@ -322,13 +322,13 @@
 fun gen_class prep_class_spec b raw_includes raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy b;
-    val prefix = Binding.qualify true "class";
     val ctxt = Proof_Context.init_global thy;
     val (((sups, supparam_names), (supsort, base_sort, supexpr)), (includes, elems, global_syntax)) =
       prep_class_spec ctxt raw_supclasses raw_includes raw_elems;
+    val of_class_binding = Binding.qualify_name true b "intro_of_class";
   in
     thy
-    |> Expression.add_locale b (prefix b) includes supexpr elems
+    |> Expression.add_locale b (Binding.qualify true "class" b) includes 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) =>
@@ -339,7 +339,7 @@
            mixin = Option.map (rpair true) eq_morph,
            export = export_morph})
     #> 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)))
+    #> Global_Theory.store_thm (of_class_binding, of_class)))
     |> snd
     |> Named_Target.init includes class
     |> pair class