diff -r cfbe9609ceb1 -r bd3486c57ba3 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Tue Jun 23 16:27:12 2009 +0200
@@ -340,7 +340,7 @@
   | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
   | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
 
-fun is_datatype thy n = is_some (Symtab.lookup (Datatype.get_datatypes thy) n);
+fun is_datatype thy = is_some o Datatype.get_info thy;
 
 fun mk_map "List.list" = Syntax.const "List.map"
   | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);