# HG changeset patch
# User wenzelm
# Date 1300801548 -3600
# Node ID dbdd4790da343dd44cc13667701a3c84be95909e
# Parent  5a505dfec04ec52f32edd1ac41bb33e5156f77f4
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);

diff -r 5a505dfec04e -r dbdd4790da34 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Tue Mar 22 14:22:40 2011 +0100
+++ b/src/CCL/Term.thy	Tue Mar 22 14:45:48 2011 +0100
@@ -40,16 +40,16 @@
   letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
 
 syntax
-  "_let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
+  "_let"     :: "[id,i,i]=>i"             ("(3let _ be _/ in _)"
                         [0,0,60] 60)
 
-  "_letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
+  "_letrec"  :: "[id,id,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
                         [0,0,0,60] 60)
 
-  "_letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
+  "_letrec2" :: "[id,id,id,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
                         [0,0,0,0,60] 60)
 
-  "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
+  "_letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
                         [0,0,0,0,0,60] 60)
 
 ML {*