# HG changeset patch
# User haftmann
# Date 1144332622 -7200
# Node ID 73439b467e757a6042d8c9af54473abe3a12d19b
# Parent  b4e00947c8a14c8a64a65f1e5ef64562d0fe2747
small type annotation fix

diff -r b4e00947c8a1 -r 73439b467e75 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Thu Apr 06 16:09:54 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Thu Apr 06 16:10:22 2006 +0200
@@ -302,8 +302,8 @@
 
 instance group_prod_def: (group, group) * :: group
   mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in
-              (x1 \<otimes> y1, x2 \<otimes> y2))"
-  mult_one_def: "\<one> == (\<one>, \<one>)"
+              ((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)"
 by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl)