# HG changeset patch
# User haftmann
# Date 1250257015 -7200
# Node ID c96330408d8910a9aa54bdc7b88773580dd7f2c4
# Parent  b0d2b49bfaede2a0e37d49e62f97539d30d463e3
formally stylized

diff -r b0d2b49bfaed -r c96330408d89 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Aug 14 15:36:54 2009 +0200
+++ b/src/HOL/Quickcheck.thy	Fri Aug 14 15:36:55 2009 +0200
@@ -54,7 +54,7 @@
 begin
 
 definition 
-  "random _ = Pair (STR [], \<lambda>u. Code_Eval.term_of (STR []))"
+  "random _ = Pair (STR '''', \<lambda>u. Code_Eval.term_of (STR ''''))"
 
 instance ..