# HG changeset patch
# User bulwahn
# Date 1316441910 -7200
# Node ID 5c8d7d6db682073e422f77b9b766e958d7110723
# Parent  0febe208942566ffdbce252a983049fb54777cbe
ensuring that some constants are generated in the source code by adding calls in ensure_testable

diff -r 0febe2089425 -r 5c8d7d6db682 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Mon Sep 19 16:18:23 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Sep 19 16:18:30 2011 +0200
@@ -356,6 +356,23 @@
 
 setup {* Narrowing_Generators.setup *}
 
+definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
+where
+  "narrowing_dummy_partial_term_of = partial_term_of"
+
+definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons"
+where
+  "narrowing_dummy_narrowing = narrowing"
+
+lemma [code]:
+  "ensure_testable f =
+    (let
+      x = narrowing_dummy_narrowing :: code_int => bool cons;
+      y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
+      z = (conv :: _ => _ => unit)  in f)"
+unfolding Let_def ensure_testable_def ..
+
+  
 subsection {* Narrowing for integers *}
 
 
@@ -436,4 +453,4 @@
 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
 
 
-end
\ No newline at end of file
+end