# HG changeset patch
# User bulwahn
# Date 1291977724 -3600
# Node ID 013adf7ebd964c5f0712a89736e69084d5519f3e
# Parent  eaefbe8aac1cfaf3f3bf59ae5d65346637564cb0
removing unneccassary sort constraints

diff -r eaefbe8aac1c -r 013adf7ebd96 src/HOL/Smallcheck.thy
--- a/src/HOL/Smallcheck.thy	Fri Dec 10 09:18:17 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Fri Dec 10 11:42:04 2010 +0100
@@ -128,7 +128,7 @@
   "check_all_n_lists f n =
      (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
 
-instantiation "fun" :: ("{equal, enum, check_all}", "{enum, term_of, check_all}") check_all
+instantiation "fun" :: ("{equal, check_all}", check_all) check_all
 begin
 
 definition mk_map_term :: "'a list \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> unit \<Rightarrow> term"