# HG changeset patch
# User wenzelm
# Date 1428000404 -7200
# Node ID 7d5b2f4c621c6f2ce4d22fb2589753e6187c3334
# Parent  0655a7217e1479657228006e709ab141daa91c5d# Parent  d1ddcd8df4e4589e00a0ee212236432bce3506ee
merged

diff -r d1ddcd8df4e4 -r 7d5b2f4c621c src/HOL/Rings.thy
--- 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
diff -r d1ddcd8df4e4 -r 7d5b2f4c621c src/Pure/Isar/class.ML
--- 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')