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/typechecking.ML | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

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

diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
index a6e1726..b7a7f9b 100644
--- a/spartan/core/typechecking.ML
+++ b/spartan/core/typechecking.ML
@@ -37,8 +37,7 @@ fun put_types typings = foldr1 (op o) (map put_type typings)
 
 (* Context tactics for type-checking *)
 
-val debug_typechk =
-  Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
+val debug_typechk = Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
 
 fun debug_tac ctxt s =
   if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac
@@ -73,9 +72,9 @@ fun check_infer_step facts i (ctxt, st) =
           map (Simplifier.norm_hhf ctxt) facts
           (*MAYBE FIXME: Remove `typechk` from this list, and instead perform
             definitional unfolding to (w?)hnf.*)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>)
+          @(Named_Theorems.get ctxt \<^named_theorems>\<open>type\<close>)
           @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>)
+          @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
           @(map #1 (Elim.rules ctxt)))
         in (resolve_from_net_tac ctxt net) i end
       else no_tac)
-- 
cgit v1.2.3