src/Pure/Isar/proof_context.ML

 (* simult_matches *)
 
 fun simult_matches ctxt (t, pats) =
   (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
     NONE => error "Pattern match failed!"
-  | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
+  | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
 
 (* bind_terms *)
 
 val bind_terms = fold (fn (xi, t) => fn ctxt =>