From dc2730916482bd230f9bd5244b8b2cc9d005f69a Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 7 Aug 2018 12:30:59 +0200
Subject: Old application syntax incompatible with Eisbach

---
 scratch.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'scratch.thy')

diff --git a/scratch.thy b/scratch.thy
index b88a8fc..55e7023 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,9 +3,9 @@ theory scratch
 
 begin
 
-abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<nat>) (\<lambda>n c. n) 0 n)"
+abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)"
 
-schematic_goal "?a : (pred`0) =\<^sub>\<nat> 0"
+schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0"
 apply (subst comp)
 apply (rule Nat_form)
 prefer 4 apply (subst comp)
-- 
cgit v1.2.3