# HG changeset patch
# User wenzelm
# Date 1256399273 -7200
# Node ID e50f948fd6bdee49f665af6ea74f118ecd81874d
# Parent  6e5b994070c1735e488a7f4c79c8d98ed6f844e4
handle Sorts.CLASS_ERROR instead of arbitrary exceptions;

diff -r 6e5b994070c1 -r e50f948fd6bd src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Oct 23 20:48:14 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Oct 24 17:47:53 2009 +0200
@@ -317,7 +317,7 @@
       |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
       |> fold meet_random insts;
   in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
-  end handle CLASS_ERROR => NONE;
+  end handle Sorts.CLASS_ERROR _ => NONE;
 
 fun ensure_random_datatype config raw_tycos thy =
   let