src/HOL/Groups.thy

--- a/src/HOL/Groups.thy	Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Groups.thy	Thu Feb 25 22:32:09 2010 +0100
@@ -1250,7 +1250,7 @@
 val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
 
 val dest_eqI = 
-  fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
+  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
 
 );
 *}