--- a/src/HOL/Quickcheck_Narrowing.thy Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Mon Jul 18 10:34:21 2011 +0200
@@ -431,9 +431,8 @@
*)
hide_type code_int narrowing_type narrowing_term cons property
-hide_const int_of of_int nth error toEnum marker empty
- C cons conv nonEmpty "apply" sum ensure_testable all exists
-hide_const (open) Var Ctr
+hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists
+hide_const (open) Var Ctr "apply" sum cons
hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def