src/HOL/Library/Transitive_Closure_Table.thy
changeset 45169 4baa475a51e6
parent 44890 22f665a2e91c
child 45231 d85a2fdc586c
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Tue Oct 18 15:40:59 2011 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Wed Oct 19 08:37:14 2011 +0200
@@ -201,22 +201,6 @@
 | "test B A"
 | "test B C"
 
-subsubsection {* Invoking with the (legacy) SML code generator *}
-
-text {* this test can be removed once the SML code generator is deactivated *}
-
-code_module Test
-contains
-test1 = "test\<^sup>*\<^sup>* A C"
-test2 = "test\<^sup>*\<^sup>* C A"
-test3 = "test\<^sup>*\<^sup>* A _"
-test4 = "test\<^sup>*\<^sup>* _ C"
-
-ML "Test.test1"
-ML "Test.test2"
-ML "DSeq.list_of Test.test3"
-ML "DSeq.list_of Test.test4"
-
 subsubsection {* Invoking with the predicate compiler and the generic code generator *}
 
 code_pred test .