# HG changeset patch # User wenzelm # Date 1369943409 -7200 # Node ID 9e97fd77a879c25c31b02f2cc0481a699b7fd976 # Parent 24f59223430da71a7a45ef0ded2694bf76713111 tuned; diff -r 24f59223430d -r 9e97fd77a879 src/HOL/Spec_Check/base_generator.ML --- 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 diff -r 24f59223430d -r 9e97fd77a879 src/HOL/Spec_Check/gen_construction.ML --- 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