diff -r 189c81779a68 -r fe9993491317 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 "\>" 60) no_notation scomp (infixl "\\" 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' ::