From 68bbcdcca00ae85dcaeae3ba7858dff1aa4802a6 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 30 May 2020 18:29:11 +0200
Subject: inhabitation coercion should be syntax, not logical constant!

---
 spartan/core/Spartan.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'spartan')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 004ba8d..9a6d884 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -294,8 +294,8 @@ val _ = Context.>>
 
 text \<open>Automatically insert inhabitation judgments where needed:\<close>
 
-consts inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
-translations "CONST inhabited A" \<rightharpoonup> "CONST has_type {} A"
+syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
+translations "inhabited A" \<rightharpoonup> "CONST has_type {} A"
 
 
 section \<open>Lambda coercion\<close>
-- 
cgit v1.2.3