1.1 --- a/src/HOL/Real/Rational.thy	Thu Aug 28 22:08:02 2008 +0200
     1.2 +++ b/src/HOL/Real/Rational.thy	Thu Aug 28 22:08:11 2008 +0200
     1.3 @@ -802,7 +802,7 @@
     1.4    then have "?c \<noteq> 0" by simp
     1.5    then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
     1.6    moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
     1.7 -   by (simp add: times_div_mod_plus_zero_one.mod_div_equality)
     1.8 +   by (simp add: semiring_div_class.mod_div_equality)
     1.9    moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    1.10    moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    1.11    ultimately show ?thesis

     2.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Aug 28 22:08:02 2008 +0200
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 28 22:08:11 2008 +0200
     2.3 @@ -803,8 +803,8 @@
     2.4      neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
     2.5      simpset = HOL_basic_ss
     2.6        addsimps
     2.7 -       [@{thm "monoid_add_class.zero_plus.add_0_left"},
     2.8 -        @{thm "monoid_add_class.zero_plus.add_0_right"},
     2.9 +       [@{thm "monoid_add_class.add_0_left"},
    2.10 +        @{thm "monoid_add_class.add_0_right"},
    2.11          @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
    2.12          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
    2.13          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},

     3.1 --- a/src/HOL/ex/Numeral.thy	Thu Aug 28 22:08:02 2008 +0200
     3.2 +++ b/src/HOL/ex/Numeral.thy	Thu Aug 28 22:08:11 2008 +0200
     3.3 @@ -397,7 +397,7 @@
     3.4  lemma of_num_plus [numeral]:
     3.5    "of_num m + of_num n = of_num (m + n)"
     3.6    by (induct n rule: num_induct)
     3.7 -    (simp_all add: Dig_plus of_num_one semigroup_add_class.plus.add_assoc [symmetric, of m]
     3.8 +    (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m]
     3.9      add_ac of_num_plus_one [symmetric])
    3.10  
    3.11  lemma of_num_times_one [numeral]:
    3.12 @@ -412,7 +412,7 @@
    3.13    "of_num m * of_num n = of_num (m * n)"
    3.14    by (induct n rule: num_induct)
    3.15      (simp_all add: of_num_plus [symmetric]
    3.16 -    semiring_class.plus_times.right_distrib right_distrib of_num_one)
    3.17 +    semiring_class.right_distrib right_distrib of_num_one)
    3.18  
    3.19  end
    3.20  

     4.1 --- a/src/HOLCF/Completion.thy	Thu Aug 28 22:08:02 2008 +0200
     4.2 +++ b/src/HOLCF/Completion.thy	Thu Aug 28 22:08:11 2008 +0200
     4.3 @@ -243,7 +243,7 @@
     4.4   apply (rule is_lub_thelub0)
     4.5    apply (rule basis_fun_lemma0, erule f_mono)
     4.6   apply (rule is_ubI, clarsimp, rename_tac a)
     4.7 - apply (rule sq_le.trans_less [OF f_mono [OF take_chain]])
     4.8 + apply (rule trans_less [OF f_mono [OF take_chain]])
     4.9   apply (rule is_ub_thelub0)
    4.10    apply (rule basis_fun_lemma0, erule f_mono)
    4.11   apply simp
    4.12 @@ -268,7 +268,7 @@
    4.13   apply (rule is_lub_thelub0)
    4.14    apply (rule basis_fun_lemma0, erule f_mono)
    4.15   apply (rule is_ubI, clarsimp, rename_tac a)
    4.16 - apply (rule sq_le.trans_less [OF f_mono [OF take_less]])
    4.17 + apply (rule trans_less [OF f_mono [OF take_less]])
    4.18   apply (erule (1) ub_imageD)
    4.19  done
    4.20  
    4.21 @@ -371,7 +371,7 @@
    4.22   apply (rule is_lub_thelub0)
    4.23    apply (rule basis_fun_lemma, erule f_mono)
    4.24   apply (rule ub_imageI, rename_tac a)
    4.25 - apply (rule sq_le.trans_less [OF less])
    4.26 + apply (rule trans_less [OF less])
    4.27   apply (rule is_ub_thelub0)
    4.28    apply (rule basis_fun_lemma, erule g_mono)
    4.29   apply (erule imageI)

     5.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 28 22:08:02 2008 +0200
     5.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 28 22:08:11 2008 +0200
     5.3 @@ -1571,22 +1571,25 @@
     5.4  
     5.5  (* naming of interpreted theorems *)
     5.6  
     5.7 -fun global_note_prefix_i kind loc (fully_qualified, prfx) params args thy =
     5.8 +fun add_param_prefixss s =
     5.9 +  (map o apfst o apfst) (NameSpace.qualified s);
    5.10 +fun drop_param_prefixss args = (map o apfst o apfst)
    5.11 +  (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
    5.12 +
    5.13 +fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
    5.14    thy
    5.15    |> Sign.qualified_names
    5.16    |> Sign.add_path (NameSpace.base loc ^ "_locale")
    5.17    |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    5.18 -  |> (if fully_qualified then Sign.add_path (space_implode "_" params) else I)
    5.19 -  |> PureThy.note_thmss kind args
    5.20 +  |> PureThy.note_thmss kind (if fully_qualified then args else drop_param_prefixss args)
    5.21    ||> Sign.restore_naming thy;
    5.22  
    5.23 -fun local_note_prefix_i kind loc (fully_qualified, prfx) params args ctxt =
    5.24 +fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
    5.25    ctxt
    5.26    |> ProofContext.qualified_names
    5.27    |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
    5.28    |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
    5.29 -  |> (if fully_qualified then ProofContext.add_path (space_implode "_" params) else I)
    5.30 -  |> ProofContext.note_thmss_i kind args
    5.31 +  |> ProofContext.note_thmss_i kind (if fully_qualified then args else drop_param_prefixss args)
    5.32    ||> ProofContext.restore_naming ctxt;
    5.33  
    5.34  
    5.35 @@ -1687,8 +1690,10 @@
    5.36        let
    5.37          val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
    5.38          val attrib = Attrib.attribute_i thy;
    5.39 -        val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args;
    5.40 -      in global_note_prefix_i kind target (fully_qualified, prfx) (map fst parms) args' thy |> snd end;
    5.41 +        val args' = args
    5.42 +          |> interpret_args thy prfx insts prems eqns atts2 exp attrib
    5.43 +          |> add_param_prefixss (space_implode "_" (map fst parms));
    5.44 +      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
    5.45    in fold activate regs thy end;
    5.46  
    5.47  
    5.48 @@ -2091,7 +2096,7 @@
    5.49            val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
    5.50                (Symtab.empty, Symtab.empty) prems eqns atts
    5.51                exp (attrib thy_ctxt) facts;
    5.52 -        in snd (note_interp kind loc (fully_qualified, prfx) [] facts' thy_ctxt) end
    5.53 +        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
    5.54        | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
    5.55  
    5.56      fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
    5.57 @@ -2266,6 +2271,7 @@
    5.58        ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
    5.59          map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
    5.60        |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
    5.61 +
    5.62      (* equations *)
    5.63      val eqn_elems = if null eqns then []
    5.64        else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
    5.65 @@ -2378,7 +2384,7 @@
    5.66                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
    5.67                  in
    5.68                    thy
    5.69 -                  |> global_note_prefix_i kind loc (fully_qualified, prfx) [] facts'
    5.70 +                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
    5.71                    |> snd
    5.72                  end
    5.73                | activate_elem _ _ thy = thy;