# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID e8f113ce8a94805e5ff7017cebf9b3853fd0d895
# Parent  af501c14d8f0f1b79464c3fc36543178b2542384
adapting Quickcheck_Narrowing and example file to new names

diff -r af501c14d8f0 -r e8f113ce8a94 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -76,13 +76,13 @@
 
 (* counterexample generator *)
   
-structure Quickcheck_Narrowing_Result = Proof_Data
+structure Counterexample = Proof_Data
 (
   type T = unit -> term list option
   fun init _ () = error " Quickcheck_Narrowing_Result"
 )
 
-val put_counterexample =  Quickcheck_Narrowing_Result.put
+val put_counterexample =  Counterexample.put
   
 fun compile_generator_expr ctxt t size =
   let
@@ -90,8 +90,7 @@
     fun ensure_testable t =
       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
     val t = dynamic_value_strict
-      (Quickcheck_Narrowing_Result.get, Quickcheck_Narrowing_Result.put,
-        "Quickcheck_Narrowing.put_counterexample")
+      (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
       thy (Option.map o map) (ensure_testable t) []
   in
     (t, NONE)
diff -r af501c14d8f0 -r e8f113ce8a94 src/HOL/ex/Quickcheck_Narrowing.thy
--- a/src/HOL/ex/Quickcheck_Narrowing.thy	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing.thy	Fri Mar 11 15:21:13 2011 +0100
@@ -1,11 +1,11 @@
-(*  Title:      HOL/ex/LSC_Examples.thy
+(*  Title:      HOL/ex/Quickcheck_Narrowing_Examples.thy
     Author:     Lukas Bulwahn
     Copyright   2011 TU Muenchen
 *)
 
-header {* Examples for invoking lazysmallcheck (LSC) *}
+header {* Examples for narrowing-based testing  *}
 
-theory LSC_Examples
+theory Quickcheck_Narrowing_Examples
 imports "~~/src/HOL/Library/LSC"
 begin
 
diff -r af501c14d8f0 -r e8f113ce8a94 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -77,7 +77,7 @@
 ];
 
 if getenv "EXEC_GHC" = "" then ()
-else use_thy "LSC_Examples";
+else use_thy "Quickcheck_Narrowing_Examples";
 
 use_thy "SVC_Oracle";
 if getenv "SVC_HOME" = "" then ()