--- a/src/HOL/Spec_Check/base_generator.ML Thu May 30 21:37:00 2013 +0200
+++ b/src/HOL/Spec_Check/base_generator.ML Thu May 30 21:47:48 2013 +0200
@@ -91,15 +91,15 @@
fun lift obj r = (obj, r)
-local open Vector (* Isabelle does not use vectors? *)
- fun explode ((freq, gen), acc) =
- List.tabulate (freq, fn _ => gen) @ acc
-in fun choose v r =
- let val (i, r) = range(0, length v - 1) r
- in sub (v, i) r
- end
- fun choose' v = choose (fromList (foldr explode nil v))
- fun select v = choose (map lift v)
+local (* Isabelle does not use vectors? *)
+ fun explode ((freq, gen), acc) =
+ List.tabulate (freq, fn _ => gen) @ acc
+in
+ 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 select v = choose (Vector.map lift v)
end
fun chooseL l = choose (Vector.fromList l)