let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
authorwenzelm
Tue, 22 Mar 2011 14:45:48 +0100
changeset 42051 dbdd4790da34
parent 42050 5a505dfec04e
child 42052 34f1d2d81284
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
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 {*