1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Sep 19 16:18:23 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Sep 19 16:18:30 2011 +0200
     1.3 @@ -356,6 +356,23 @@
     1.4  
     1.5  setup {* Narrowing_Generators.setup *}
     1.6  
     1.7 +definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
     1.8 +where
     1.9 +  "narrowing_dummy_partial_term_of = partial_term_of"
    1.10 +
    1.11 +definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons"
    1.12 +where
    1.13 +  "narrowing_dummy_narrowing = narrowing"
    1.14 +
    1.15 +lemma [code]:
    1.16 +  "ensure_testable f =
    1.17 +    (let
    1.18 +      x = narrowing_dummy_narrowing :: code_int => bool cons;
    1.19 +      y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
    1.20 +      z = (conv :: _ => _ => unit)  in f)"
    1.21 +unfolding Let_def ensure_testable_def ..
    1.22 +
    1.23 +  
    1.24  subsection {* Narrowing for integers *}
    1.25  
    1.26  
    1.27 @@ -436,4 +453,4 @@
    1.28  hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
    1.29  
    1.30  
    1.31 -end
    1.32 \ No newline at end of file
    1.33 +end