diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean
index 16b041d0..dd797435 100644
--- a/Aesop/Builder/Forward.lean
+++ b/Aesop/Builder/Forward.lean
@@ -60,7 +60,7 @@ def getImmediatePremises  (type : Expr) (pat? : Option RulePattern)
       for h : i in [:args.size] do
         if isPatternInstantiated i then
           continue
-        let fvarId := (args[i]'h.2).fvarId!
+        let fvarId := args[i].fvarId!
         let ldecl ← fvarId.getDecl
         let isNondep : MetaM Bool :=
           args.allM (start := i + 1) λ arg => do
diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean
index 5c7cfc4c..fd18c6f3 100644
--- a/Aesop/RuleTac/Forward.lean
+++ b/Aesop/RuleTac/Forward.lean
@@ -33,7 +33,7 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern)
     let mut instMVars := Array.mkEmpty argMVars.size
     let mut immediateMVars := Array.mkEmpty argMVars.size
     for h : i in [:argMVars.size] do
-      let mvarId := argMVars[i]'h.2 |>.mvarId!
+      let mvarId := argMVars[i].mvarId!
       if patInstantiatedMVars.contains mvarId then
         continue
       if immediate.contains i then
diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean
index dbbafb8a..751c7da9 100644
--- a/Aesop/Script/StructureDynamic.lean
+++ b/Aesop/Script/StructureDynamic.lean
@@ -60,7 +60,7 @@ def DynStructureM.run (x : DynStructureM α) (script : UScript) :
     MetaM (α × Bool) := do
   let mut steps : PHashMap MVarId (Nat × Step) := {}
   for h : i in [:script.size] do
-    let step := script[i]'h.2
+    let step := script[i]
     steps := steps.insert step.preGoal (i, step)
   let (a, s) ← ReaderT.run x { steps } |>.run {}
   return (a, s.perfect)
diff --git a/Aesop/Script/StructureStatic.lean b/Aesop/Script/StructureStatic.lean
index ccfca1b0..b111ce10 100644
--- a/Aesop/Script/StructureStatic.lean
+++ b/Aesop/Script/StructureStatic.lean
@@ -22,7 +22,7 @@ protected def StaticStructureM.run (script : UScript) (x : StaticStructureM α)
     CoreM (α × Bool) := do
   let mut steps : Std.HashMap MVarId (Nat × Step) := Std.HashMap.empty script.size
   for h : i in [:script.size] do
-    let step := script[i]'h.2
+    let step := script[i]
     if h : step.postGoals.size = 1 then
       if step.postGoals[0].goal == step.preGoal then
         continue
diff --git a/Aesop/Search/Expansion.lean b/Aesop/Search/Expansion.lean
index 729ee123..7b28ff92 100644
--- a/Aesop/Search/Expansion.lean
+++ b/Aesop/Search/Expansion.lean
@@ -69,7 +69,7 @@ def addRapps (parentRef : GoalRef) (rule : RegularRule)
   let mut rrefs := Array.mkEmpty rapps.size
   let mut subgoals := Array.mkEmpty $ rapps.size * 3
   for h : i in [:rapps.size] do
-    let rapp := rapps[i]'h.2
+    let rapp := rapps[i]
     let successProbability :=
       parent.successProbability *
       (rapp.successProbability?.getD rule.successProbability)