From 6464ab52b593ceb9d92b9c0c38df32c049537262 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 21 Jul 2020 19:31:31 +0200
Subject: minor

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

(limited to 'spartan')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index fa6148f..8c87c2e 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -462,7 +462,7 @@ lemma id_right [comp]:
 
 lemma id_U [typechk]:
   "id (U i): U i \<rightarrow> U i"
-  by typechk (rule Ui_in_USi) (*FIXME: Add annotation rule to typechecker*)
+  using Ui_in_USi by typechk
 
 
 section \<open>Pairs\<close>
-- 
cgit v1.2.3