# HG changeset patch
# User bulwahn
# Date 1290418916 -3600
# Node ID 3bd9512ca486f929c586869682bd323139976dee
# Parent  47004929bc71cc1e62c37926313ceb1f4bf522c6
renaming quickcheck generator code to random

diff -r 47004929bc71 -r 3bd9512ca486 NEWS
--- a/NEWS	Mon Nov 22 10:41:55 2010 +0100
+++ b/NEWS	Mon Nov 22 10:41:56 2010 +0100
@@ -89,6 +89,9 @@
 
 *** HOL ***
 
+* Quickcheck's generator for random generation is renamed from "code" to
+"random". INCOMPATIBILITY. 
+
 * Theory Multiset provides stable quicksort implementation of sort_key.
 
 * Quickcheck now has a configurable time limit which is set to 30 seconds
diff -r 47004929bc71 -r 3bd9512ca486 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 10:41:55 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 10:41:56 2010 +0100
@@ -413,6 +413,6 @@
   Datatype.interpretation ensure_random_datatype
   #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
   #> Context.theory_map
-    (Quickcheck.add_generator ("code", compile_generator_expr));
+    (Quickcheck.add_generator ("random", compile_generator_expr));
 
 end;