# HG changeset patch
# User blanchet
# Date 1346756549 -7200
# Node ID c9c09dbdbd1c4e7e6968c02216194ce283a336c2
# Parent  c0d77c85e0b8f74e01a3831c50ee1ff47c374f0c
removed oddities

diff -r c0d77c85e0b8 -r c9c09dbdbd1c src/HOL/Codatatype/Examples/Misc_Codata.thy
--- 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"
diff -r c0d77c85e0b8 -r c9c09dbdbd1c src/HOL/Codatatype/Examples/Misc_Data.thy
--- 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"