1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -76,13 +76,13 @@
     1.4  
     1.5  (* counterexample generator *)
     1.6    
     1.7 -structure Quickcheck_Narrowing_Result = Proof_Data
     1.8 +structure Counterexample = Proof_Data
     1.9  (
    1.10    type T = unit -> term list option
    1.11    fun init _ () = error " Quickcheck_Narrowing_Result"
    1.12  )
    1.13  
    1.14 -val put_counterexample =  Quickcheck_Narrowing_Result.put
    1.15 +val put_counterexample =  Counterexample.put
    1.16    
    1.17  fun compile_generator_expr ctxt t size =
    1.18    let
    1.19 @@ -90,8 +90,7 @@
    1.20      fun ensure_testable t =
    1.21        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.22      val t = dynamic_value_strict
    1.23 -      (Quickcheck_Narrowing_Result.get, Quickcheck_Narrowing_Result.put,
    1.24 -        "Quickcheck_Narrowing.put_counterexample")
    1.25 +      (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.26        thy (Option.map o map) (ensure_testable t) []
    1.27    in
    1.28      (t, NONE)

     2.1 --- a/src/HOL/ex/Quickcheck_Narrowing.thy	Fri Mar 11 15:21:13 2011 +0100
     2.2 +++ b/src/HOL/ex/Quickcheck_Narrowing.thy	Fri Mar 11 15:21:13 2011 +0100
     2.3 @@ -1,11 +1,11 @@
     2.4 -(*  Title:      HOL/ex/LSC_Examples.thy
     2.5 +(*  Title:      HOL/ex/Quickcheck_Narrowing_Examples.thy
     2.6      Author:     Lukas Bulwahn
     2.7      Copyright   2011 TU Muenchen
     2.8  *)
     2.9  
    2.10 -header {* Examples for invoking lazysmallcheck (LSC) *}
    2.11 +header {* Examples for narrowing-based testing  *}
    2.12  
    2.13 -theory LSC_Examples
    2.14 +theory Quickcheck_Narrowing_Examples
    2.15  imports "~~/src/HOL/Library/LSC"
    2.16  begin
    2.17  

     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Mar 11 15:21:13 2011 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Mar 11 15:21:13 2011 +0100
     3.3 @@ -77,7 +77,7 @@
     3.4  ];
     3.5  
     3.6  if getenv "EXEC_GHC" = "" then ()
     3.7 -else use_thy "LSC_Examples";
     3.8 +else use_thy "Quickcheck_Narrowing_Examples";
     3.9  
    3.10  use_thy "SVC_Oracle";
    3.11  if getenv "SVC_HOME" = "" then ()