# HG changeset patch
# User bulwahn
# Date 1300102451 -3600
# Node ID 328371f4f927b2a708167e7610ba99bb04dcd23e
# Parent  13904699c85981f7ef5413550baf7e2ac86ad013
removing definition of cons0; hiding constants in Quickcheck_Narrowing

diff -r 13904699c859 -r 328371f4f927 src/HOL/Library/Quickcheck_Narrowing.thy
--- a/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Mar 14 12:34:10 2011 +0100
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Mar 14 12:34:11 2011 +0100
@@ -171,10 +171,6 @@
     unfolding apply_def by (auto split: cons.split type.split simp add: Let_def)
 qed
 
-definition cons0 :: "'a => 'a narrowing"
-where
-  "cons0 f = cons f"
-
 type_synonym pos = "code_int list"
 (*
 subsubsection {* Term refinement *}
@@ -216,7 +212,7 @@
 begin
 
 definition
-  "narrowing = cons0 ()"
+  "narrowing = cons ()"
 
 instance ..
 
@@ -226,7 +222,7 @@
 begin
 
 definition
-  "narrowing = sum (cons0 True) (cons0 False)" 
+  "narrowing = sum (cons True) (cons False)" 
 
 instance ..
 
@@ -236,7 +232,7 @@
 begin
 
 definition
-  "narrowing = sum (cons0 None) (cons1 Some)"
+  "narrowing = sum (cons None) (cons1 Some)"
 
 instance ..
 
@@ -348,6 +344,8 @@
 
 setup {* Narrowing_Generators.setup *}
 
-hide_const (open) empty
+hide_type (open) code_int type "term" cons
+hide_const (open) int_of of_int nth error toEnum map_index split_At empty
+  cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
 
 end
\ No newline at end of file