src/Pure/Tools/rule_insts.ML

     fun zip_vars _ [] = []
       | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
       | zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest
       | zip_vars [] _ = error "More instantiations than variables in theorem";
     val insts =
-      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
-      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
+      zip_vars (build_rev (Term.add_vars (Thm.full_prop_of thm))) args @
+      zip_vars (build_rev (Term.add_vars (Thm.concl_of thm))) concl_args;
   in where_rule ctxt insts fixes thm end;
 
 fun read_instantiate ctxt insts xs =
   where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs);