Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ported 'Statespace' to support new datatypes as well
authorblanchet
Wed, 03 Sep 2014 00:06:22 +0200
changeset 58149 72fc2bf52986
parent 58148 9764b994a421
child 58150 2bf3ed0f62cf
ported 'Statespace' to support new datatypes as well
src/HOL/Statespace/state_fun.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle