From 09137c701928a51b57dc1f2a868610e861cf4e55 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 22 Feb 2023 17:55:46 +0100
Subject: [PATCH] remove `set_option tactic.hygienic false`

---
 server/leanserver/GameServer/FileWorker.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index 11ee719..a82ea56 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -150,9 +150,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
 
-          let cmdStx ← `(command|
-            set_option tactic.hygienic false in
-            theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+          let cmdStx ← `(command| theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
 
           Elab.Command.withScope (fun _ => level.scope) do -- use open namespaces and options as in the file
             Elab.Command.elabCommandTopLevel cmdStx)