# HG changeset patch
# User blanchet
# Date 1409695582 -7200
# Node ID 72fc2bf5298615bebcb69ebfab1e1fe71c1b6765
# Parent  9764b994a4212930f92147784e86e143e4c8ebbe
ported 'Statespace' to support new datatypes as well

diff -r 9764b994a421 -r 72fc2bf52986 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Wed Sep 03 00:06:21 2014 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Wed Sep 03 00:06:22 2014 +0200
@@ -339,7 +339,7 @@
   | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
   | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
 
-fun is_datatype thy = is_some o Old_Datatype_Data.get_info thy;
+fun is_datatype thy = is_some o BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting;
 
 fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map}
   | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);