hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
authorhuffman
Fri, 02 Dec 2011 10:31:47 +0100
changeset 45734 1024dd30da42
parent 45733 6bb30ae1abfe
child 45735 7d7d7af647a9
hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Dec 01 22:16:26 2011 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Dec 02 10:31:47 2011 +0100
@@ -348,7 +348,7 @@
   "eval_cfun (Constant c) y = c"
 
 hide_type (open) cfun
-hide_const (open) Constant eval_cfun
+hide_const (open) Constant eval_cfun Abs_cfun Rep_cfun
 
 subsubsection {* Setting up the counterexample generator *}