src/HOL/List.thy
changeset 43324 2b47822868e4
parent 42871 1c0b99f950d9
child 43580 023a1d1f97bd
     1.1 --- a/src/HOL/List.thy	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -383,7 +383,8 @@
     1.4  
     1.5    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
     1.6      let
     1.7 -      val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
     1.8 +      (* FIXME proper name context!? *)
     1.9 +      val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
    1.10        val e = if opti then singl e else e;
    1.11        val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
    1.12        val case2 =