diff -r 6f43714517ee -r 08c8dad8e399 src/HOL/Matrix/codegen_prep.ML
--- a/src/HOL/Matrix/codegen_prep.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Matrix/codegen_prep.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -74,8 +74,8 @@
 	val key = f x
     in
 	case assoc (g, key) of
-	    None => (key, [x])::g
-	  | Some l => overwrite (g, (key, x::l))
+	    NONE => (key, [x])::g
+	  | SOME l => overwrite (g, (key, x::l))
     end
     
 fun prepare_thms ths =