--- a/src/HOL/List.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/List.thy Thu Jun 09 16:34:49 2011 +0200
@@ -383,7 +383,8 @@
fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
let
- val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
+ (* FIXME proper name context!? *)
+ val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
val e = if opti then singl e else e;
val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
val case2 =