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/goals.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 540f5c7..a04bd0e 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -151,7 +151,7 @@ fun gen_schematic_theorem
                 map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res
             in
               Local_Theory.notes_kind kind
-                [((name, @{attributes [typechk]} @ atts),
+                [((name, @{attributes [type]} @ atts),
                   [(maps #2 res_folded, [])])]
                 new_lthy
             end
-- 
cgit v1.2.3