removing quickcheck tester SML-inductive based on the old code generator
authorbulwahn
Wed, 19 Oct 2011 08:37:24 +0200
changeset 45178 fe9993491317
parent 45177 189c81779a68
child 45179 6f705c69678f
removing quickcheck tester SML-inductive based on the old code generator
src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Wed Oct 19 08:37:23 2011 +0200
+++ b/src/HOL/Quickcheck.thy	Wed Oct 19 08:37:24 2011 +0200
@@ -144,13 +144,6 @@
 no_notation fcomp (infixl "\<circ>>" 60)
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
-subsection {* Tester SML-inductive based on the SML code generator *}
-
-setup {*
-  Context.theory_map (Quickcheck.add_tester ("SML_inductive",
-    (Inductive_Codegen.active, Quickcheck_Common.generator_test_goal_terms Inductive_Codegen.test_term)));
-*}
-
 subsection {* The Random-Predicate Monad *} 
 
 fun iter' ::