From 1a860059b22c0cffa6f2b294351338dd3a193628 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 15 Dec 2024 19:34:32 +1100
Subject: [PATCH] fixes

---
 Aesop/RulePattern.lean | 6 +++---
 Aesop/Script/Util.lean | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Aesop/RulePattern.lean b/Aesop/RulePattern.lean
index 6de12d8e..7c73ec24 100644
--- a/Aesop/RulePattern.lean
+++ b/Aesop/RulePattern.lean
@@ -144,7 +144,7 @@ def openRuleType (pat : RulePattern) (inst : RulePatternInstantiation)
   let mut assigned := ∅
   for h : i in [:mvars.size] do
     if let some inst ← pat.getInstantiation inst i then
-      let mvarId := mvars[i]'h.2 |>.mvarId!
+      let mvarId := mvars[i] |>.mvarId!
       -- We use `isDefEq` to make sure that universe metavariables occurring in
       -- the type of `mvarId` are assigned.
       if ← isDefEq (.mvar mvarId) inst then
@@ -163,7 +163,7 @@ def specializeRule (pat : RulePattern) (inst : RulePatternInstantiation)
         if let some inst ← pat.getInstantiation inst i then
           args := args.push $ some inst
         else
-          let fvarId := fvarIds[i]'h.2
+          let fvarId := fvarIds[i]
           args := args.push $ some fvarId
           remainingFVarIds := remainingFVarIds.push fvarId
       let result ← mkLambdaFVars remainingFVarIds (← mkAppOptM' rule args)
@@ -207,7 +207,7 @@ where
     let e := s.lctx.mkLambda s.fvars e
     let mut mvarIdToPos := ∅
     for h : i in [:s.fvars.size] do
-      let name := s.lctx.get! (s.fvars[i]'h.2).fvarId! |>.userName
+      let name := s.lctx.get! (s.fvars[i]).fvarId! |>.userName
       mvarIdToPos := mvarIdToPos.insert ⟨name⟩ i
     let result :=
       { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e }
diff --git a/Aesop/Script/Util.lean b/Aesop/Script/Util.lean
index 057e8bec..56866848 100644
--- a/Aesop/Script/Util.lean
+++ b/Aesop/Script/Util.lean
@@ -18,7 +18,7 @@ def findFirstStep? {α β : Type} (goals : Array α) (step? : α → Option β)
      (stepOrder : β → Nat) : Option (Nat × α × β) := Id.run do
   let mut firstStep? := none
   for h : pos in [:goals.size] do
-    let g := goals[pos]'h.2
+    let g := goals[pos]
     if let some step := step? g then
       if let some (_, _, currentFirstStep) := firstStep? then
         if stepOrder step < stepOrder currentFirstStep then