aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to 'spartan')
-rw-r--r--spartan/core/Spartan.thy4
1 files changed, 2 insertions, 2 deletions
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>