| changeset 49115 | c9c09dbdbd1c |
| parent 49074 | d8af889dcbe3 |
| child 49157 | 6407346b74c7 |
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy Tue Sep 04 13:02:28 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Tue Sep 04 13:02:29 2012 +0200 @@ -12,10 +12,6 @@ imports "../Codatatype" begin -ML {* quick_and_dirty := false *} - -ML {* PolyML.fullGC (); *} - data_raw simple: 'a = "unit + unit + unit + unit" data_raw mylist: 'list = "unit + 'a \<times> 'list"