tuned;

--- a/src/HOL/Spec_Check/base_generator.ML	Thu May 30 21:47:48 2013 +0200
+++ b/src/HOL/Spec_Check/base_generator.ML	Thu May 30 21:50:09 2013 +0200
@@ -98,7 +98,7 @@
   fun choose v r =
     let val (i, r) = range(0, Vector.length v - 1) r
     in Vector.sub (v, i) r end
-  fun choose' v = choose (Vector.fromList (Vector.foldr explode nil v))
+  fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
   fun select v = choose (Vector.map lift v)
 end
 
@@ -132,7 +132,7 @@
 
 fun list flip g r =
   case flip r of
-      (true, r) => (nil, r)
+      (true, r) => ([], r)
     | (false, r) =>
       let
         val (x,r) = g r

--- a/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 21:47:48 2013 +0200
+++ b/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 21:50:09 2013 +0200
@@ -38,7 +38,7 @@
 val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
 
 (*Turn a type list into a nested Con*)
-fun make_con nil = raise Empty
+fun make_con [] = raise Empty
   | make_con [c] = c
   | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
 
@@ -61,7 +61,7 @@
   || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
   >> (make_con o rev)) s
 
-and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, nil)))) s
+and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
 
 and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s