src/Pure/Isar/element.ML

 fun standard_elim ctxt th =
   (case Object_Logic.elim_concl ctxt th of
     SOME C =>
       let
         val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
-        val insts = (TVars.empty, Vars.make [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]);
+        val insts = (TVars.empty, Vars.make1 (Term.dest_Var C, Thm.cterm_of ctxt thesis));
         val th' = Thm.instantiate insts th;
       in (th', true) end
   | NONE => (th, false));
 
 fun thm_name ctxt kind th prts =