--- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Tue Sep 04 13:02:28 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Tue Sep 04 13:02:29 2012 +0200
@@ -12,10 +12,6 @@
imports "../Codatatype"
begin
-ML {* quick_and_dirty := false *}
-
-ML {* PolyML.fullGC (); *}
-
codata_raw simple: 'a = "unit + unit + unit + unit"
codata_raw stream: 's = "'a \<times> 's"
--- 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"