From 77df99b3ffa41395ced31785074525c85e35fee9 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 14 Aug 2020 19:55:38 +0200
Subject: minor

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

(limited to 'spartan/core/Spartan.thy')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 411eedd..10caa30 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -362,6 +362,8 @@ translations
   "_lam_i2 x b" \<rightharpoonup> "\<lambda>x. b"
   "\<lambda>x. b"    \<rightleftharpoons> "CONST lam_i (fn x. b)"
 
+translations "\<lambda>x. b" \<leftharpoondown> "\<lambda>x: A. b"
+
 subsection \<open>Lambda coercion\<close>
 
 \<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
-- 
cgit v1.2.3