# HG changeset patch
# User bulwahn
# Date 1319006244 -7200
# Node ID fe9993491317ef5a4ace989a32a2871287df6c53
# Parent  189c81779a683a5f96693d9911bd8cad40a428a5
removing quickcheck tester SML-inductive based on the old code generator

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 "\<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' ::