From 77aa10763429d2ded040071fbf7bee331dd52f5e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 31 Jul 2020 18:10:10 +0200
Subject: (REF) Tweak attribute names in preparation for new logical
 introduction rule behavior

---
 spartan/core/tactics.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'spartan/core/tactics.ML')

diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 19d3d71..959050e 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -57,7 +57,7 @@ end
 
 (*Applies some introduction rule*)
 fun intro_ctac i (ctxt, st) = TACTIC_CONTEXT ctxt (resolve_tac ctxt
-  (Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>) i st)
+  (Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) i st)
 
 
 (* Induction/elimination *)
-- 
cgit v1.2.3