diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Complex/NSCA.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -11,10 +11,11 @@
 
 definition
    (* standard complex numbers reagarded as an embedded subset of NS complex *)
-   SComplex  :: "hcomplex set"
+   SComplex  :: "hcomplex set" where
    "SComplex = {x. \<exists>r. x = hcomplex_of_complex r}"
 
-   stc :: "hcomplex => hcomplex"
+definition
+   stc :: "hcomplex => hcomplex" where
     --{* standard part map*}
    "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"