--- 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);