diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index f6080f6dfe..4a71e6660a 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -63,7 +63,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
     let decl ← getMVarDecl g
     let (val, gs') ← elabTermWithHoles stx decl.type tagSuffix allowNaturalHoles
     assignExprMVar g val
-    setGoals (gs ++ gs')
+    setGoals (gs' ++ gs)
 
 @[builtinTactic «refine»] def evalRefine : Tactic := fun stx =>
   match stx with
diff --git a/tests/lean/run/269.lean b/tests/lean/run/269.lean
new file mode 100644
index 0000000000..e4cf1999df
--- /dev/null
+++ b/tests/lean/run/269.lean
@@ -0,0 +1,15 @@
+theorem haveWithSubgoals {a b : α} : a = b ↔ b = a := by
+    apply Iff.intro
+    intro h
+    have h' := h.symm
+    exact h'
+    intro h
+    exact h.symm
+
+theorem haveWithSubgoals2 {a b : α} : a = b ↔ b = a := by {
+    apply Iff.intro;
+    intro h;
+    have h' := h.symm;
+    exact h';
+    intro h; exact h.symm;
+}