merged

--- a/src/HOL/Rings.thy	Thu Apr 02 20:28:30 2015 +0200
+++ b/src/HOL/Rings.thy	Thu Apr 02 20:46:44 2015 +0200
@@ -502,7 +502,7 @@
 
 end
 
-class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
+class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors
 
 class idom = comm_ring_1 + semiring_no_zero_divisors
 begin

--- a/src/Pure/Isar/class.ML	Thu Apr 02 20:28:30 2015 +0200
+++ b/src/Pure/Isar/class.ML	Thu Apr 02 20:46:44 2015 +0200
@@ -384,11 +384,13 @@
     val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     val c' = Sign.full_name thy b;
     val ty' = map Term.fastype_of dangling_term_params ---> Term.fastype_of rhs';
+    val ty'' = Morphism.typ phi ty';
+    val rhs'' = map_types (Morphism.typ phi) (fold lambda dangling_term_params rhs');
   in
     thy
-    |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global (fold lambda dangling_term_params rhs'))
+    |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs'')
     |> snd
-    |> Sign.notation true prmode [(Const (c', ty'), mx)]
+    |> Sign.notation true prmode [(Const (c', ty''), mx)]
     |> (null dangling_term_params andalso not (#1 prmode = Print_Mode.input))
       ? register_operation class (c', rhs')
     |> Sign.add_const_constraint (c', SOME ty')