src/HOL/List.thy

 
   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);
       val e = if opti then singl e else e;
-      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
+      val case1 = Syntax.const @{syntax_const "_case1"} $ Syntax.strip_positions p $ e;
       val case2 =
         Syntax.const @{syntax_const "_case1"} $
           Syntax.const @{const_syntax dummy_pattern} $ NilC;
       val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
       val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];