diff -Naur Agda-1.0.2/src/BasicEngineOps.hs-boot Agda-1.0.2.new/src/BasicEngineOps.hs-boot
--- Agda-1.0.2/src/BasicEngineOps.hs-boot	2006-12-25 18:47:26.000000000 -0500
+++ Agda-1.0.2.new/src/BasicEngineOps.hs-boot	2008-07-26 06:29:02.000000000 -0400
@@ -1,4 +1,4 @@
-module BasicEngineOps where
+module BasicEngineOps (checkAndUpdate, solveCs) where
 import MetaVars(MetaVar)
 import ISynType(Exp)
 import ProofMonad(PCM)
diff -Naur Agda-1.0.2/src/Id.hs Agda-1.0.2.new/src/Id.hs
--- Agda-1.0.2/src/Id.hs	2006-12-25 18:47:26.000000000 -0500
+++ Agda-1.0.2.new/src/Id.hs	2008-07-26 06:28:22.000000000 -0400
@@ -157,7 +157,7 @@
     "$"   -> FInfixr 0
     ">>"  -> FInfixl 1
     ">>=" -> FInfixl 1
-    "×"   -> FInfixr 1
+    "\xD7"-> FInfixr 1 -- times
     "||"  -> FInfixr 2
     "&&"  -> FInfixr 3
     "=="  -> FInfix  4
@@ -172,8 +172,8 @@
     "-"   -> FInfixl 6
     "*"   -> FInfixl 7
     "/"   -> FInfixl 7
-    "·"   -> FInfixr 8
-    "°"   -> FInfixr 8
+    "\xB7"-> FInfixr 8 -- cdot
+    "\xB0"-> FInfixr 8 -- circ
     _     -> FInfixl 9
 
 
diff -Naur Agda-1.0.2/src/Lex.hs Agda-1.0.2.new/src/Lex.hs
--- Agda-1.0.2/src/Lex.hs	2006-12-25 18:47:26.000000000 -0500
+++ Agda-1.0.2.new/src/Lex.hs	2008-07-26 06:35:10.000000000 -0400
@@ -307,7 +307,7 @@
 isSym '>' = True; isSym '\\' = True; isSym '^' = True
 isSym '|' = True; isSym ':'  = True; isSym '-' = True; isSym '~' = True
 isSym ',' = True
-isSym c | c >= '\x80' = c `elem` "¡¢£¤¥¦§¨©ª«¬­®¯°±²³´µ¶·¸¹º»¼½¾¿×÷"
+isSym c | c >= '\x80' = ord c `elem` ([161..191] ++ [215,247])
 --isSym c | c >= '\x80' = isSymbol c
 isSym _   = False
 
diff -Naur Agda-1.0.2/src/PreStrings.hs Agda-1.0.2.new/src/PreStrings.hs
--- Agda-1.0.2/src/PreStrings.hs	2006-12-25 18:47:26.000000000 -0500
+++ Agda-1.0.2.new/src/PreStrings.hs	2008-07-26 06:28:36.000000000 -0400
@@ -46,6 +46,6 @@
   "Setoid","Elem","Equal","ref","sym",
   "tran","El","Eq", "_V", "A", 
   "B", "x", "xs", "m","JMeq", 
-  "same", "a", "b", "×"
+  "same", "a", "b", "\xD7" -- times
  ]