src/HOL/Hyperreal/hypreal_arith.ML

--- a/src/HOL/Hyperreal/hypreal_arith.ML	Tue Sep 07 11:42:50 2004 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML	Tue Sep 07 13:41:30 2004 +0200
@@ -35,7 +35,6 @@
     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
     simpset = simpset}),
   arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT),
-  arith_discrete ("HyperDef.hypreal",false),
   Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]];
 
 end;