# HG changeset patch
# User haftmann
# Date 1151395784 -7200
# Node ID d58e2c564100e7c37daab78990b95866ff5596ca
# Parent  fd74bf4e603ed707a01aad0af75d57ff17b00fff
slight improvement

diff -r fd74bf4e603e -r d58e2c564100 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Tue Jun 27 10:09:39 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Tue Jun 27 10:09:44 2006 +0200
@@ -304,7 +304,7 @@
   mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in
               ((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))"
   mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)"
-  mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
+  mult_inv_def: "\<div> x == let (x1::'a::group, x2::'b::group) = x in (\<div> x1, \<div> x2)"
 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
 
 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm