# HG changeset patch
# User haftmann
# Date 1219954091 -7200
# Node ID a2106c0d8c45a0713ee5e70800d53c9d0c412dc7
# Parent  4dc09699cf93f6a03d01a94dea544bd7a9cd1392
no parameter prefix for class interpretation

diff -r 4dc09699cf93 -r a2106c0d8c45 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Aug 28 22:08:02 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Thu Aug 28 22:08:11 2008 +0200
@@ -802,7 +802,7 @@
   then have "?c \<noteq> 0" by simp
   then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
   moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
-   by (simp add: times_div_mod_plus_zero_one.mod_div_equality)
+   by (simp add: semiring_div_class.mod_div_equality)
   moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
   moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
   ultimately show ?thesis
diff -r 4dc09699cf93 -r a2106c0d8c45 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Aug 28 22:08:02 2008 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 28 22:08:11 2008 +0200
@@ -803,8 +803,8 @@
     neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
     simpset = HOL_basic_ss
       addsimps
-       [@{thm "monoid_add_class.zero_plus.add_0_left"},
-        @{thm "monoid_add_class.zero_plus.add_0_right"},
+       [@{thm "monoid_add_class.add_0_left"},
+        @{thm "monoid_add_class.add_0_right"},
         @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
         @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
         @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
diff -r 4dc09699cf93 -r a2106c0d8c45 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Thu Aug 28 22:08:02 2008 +0200
+++ b/src/HOL/ex/Numeral.thy	Thu Aug 28 22:08:11 2008 +0200
@@ -397,7 +397,7 @@
 lemma of_num_plus [numeral]:
   "of_num m + of_num n = of_num (m + n)"
   by (induct n rule: num_induct)
-    (simp_all add: Dig_plus of_num_one semigroup_add_class.plus.add_assoc [symmetric, of m]
+    (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m]
     add_ac of_num_plus_one [symmetric])
 
 lemma of_num_times_one [numeral]:
@@ -412,7 +412,7 @@
   "of_num m * of_num n = of_num (m * n)"
   by (induct n rule: num_induct)
     (simp_all add: of_num_plus [symmetric]
-    semiring_class.plus_times.right_distrib right_distrib of_num_one)
+    semiring_class.right_distrib right_distrib of_num_one)
 
 end
 
diff -r 4dc09699cf93 -r a2106c0d8c45 src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Thu Aug 28 22:08:02 2008 +0200
+++ b/src/HOLCF/Completion.thy	Thu Aug 28 22:08:11 2008 +0200
@@ -243,7 +243,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule sq_le.trans_less [OF f_mono [OF take_chain]])
+ apply (rule trans_less [OF f_mono [OF take_chain]])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply simp
@@ -268,7 +268,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule sq_le.trans_less [OF f_mono [OF take_less]])
+ apply (rule trans_less [OF f_mono [OF take_less]])
  apply (erule (1) ub_imageD)
 done
 
@@ -371,7 +371,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma, erule f_mono)
  apply (rule ub_imageI, rename_tac a)
- apply (rule sq_le.trans_less [OF less])
+ apply (rule trans_less [OF less])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma, erule g_mono)
  apply (erule imageI)
diff -r 4dc09699cf93 -r a2106c0d8c45 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 28 22:08:02 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 28 22:08:11 2008 +0200
@@ -1571,22 +1571,25 @@
 
 (* naming of interpreted theorems *)
 
-fun global_note_prefix_i kind loc (fully_qualified, prfx) params args thy =
+fun add_param_prefixss s =
+  (map o apfst o apfst) (NameSpace.qualified s);
+fun drop_param_prefixss args = (map o apfst o apfst)
+  (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
+
+fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
   thy
   |> Sign.qualified_names
   |> Sign.add_path (NameSpace.base loc ^ "_locale")
   |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
-  |> (if fully_qualified then Sign.add_path (space_implode "_" params) else I)
-  |> PureThy.note_thmss kind args
+  |> PureThy.note_thmss kind (if fully_qualified then args else drop_param_prefixss args)
   ||> Sign.restore_naming thy;
 
-fun local_note_prefix_i kind loc (fully_qualified, prfx) params args ctxt =
+fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
   ctxt
   |> ProofContext.qualified_names
   |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
   |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
-  |> (if fully_qualified then ProofContext.add_path (space_implode "_" params) else I)
-  |> ProofContext.note_thmss_i kind args
+  |> ProofContext.note_thmss_i kind (if fully_qualified then args else drop_param_prefixss args)
   ||> ProofContext.restore_naming ctxt;
 
 
@@ -1687,8 +1690,10 @@
       let
         val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
         val attrib = Attrib.attribute_i thy;
-        val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args;
-      in global_note_prefix_i kind target (fully_qualified, prfx) (map fst parms) args' thy |> snd end;
+        val args' = args
+          |> interpret_args thy prfx insts prems eqns atts2 exp attrib
+          |> add_param_prefixss (space_implode "_" (map fst parms));
+      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   in fold activate regs thy end;
 
 
@@ -2091,7 +2096,7 @@
           val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
               (Symtab.empty, Symtab.empty) prems eqns atts
               exp (attrib thy_ctxt) facts;
-        in snd (note_interp kind loc (fully_qualified, prfx) [] facts' thy_ctxt) end
+        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
       | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
 
     fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
@@ -2266,6 +2271,7 @@
       ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
         map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
       |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
+
     (* equations *)
     val eqn_elems = if null eqns then []
       else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
@@ -2378,7 +2384,7 @@
                     |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
                 in
                   thy
-                  |> global_note_prefix_i kind loc (fully_qualified, prfx) [] facts'
+                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
                   |> snd
                 end
               | activate_elem _ _ thy = thy;