1.1 --- a/src/HOL/Integ/Int.ML	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Integ/Int.ML	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4    val eq_diff_eq	= eq_zdiff_eq
     1.5    val eqI_rules		= [zless_eqI, zeq_eqI, zle_eqI]
     1.6    fun dest_eqI th = 
     1.7 -      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
     1.8 +      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
     1.9  	      (HOLogic.dest_Trueprop (concl_of th)))
    1.10  
    1.11    val diff_def		= zdiff_def