let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
authorwenzelm
Tue Mar 22 14:45:48 2011 +0100 (2011-03-22)
changeset 42051dbdd4790da34
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
     1.1 --- a/src/CCL/Term.thy	Tue Mar 22 14:22:40 2011 +0100
     1.2 +++ b/src/CCL/Term.thy	Tue Mar 22 14:45:48 2011 +0100
     1.3 @@ -40,16 +40,16 @@
     1.4    letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
     1.5  
     1.6  syntax
     1.7 -  "_let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
     1.8 +  "_let"     :: "[id,i,i]=>i"             ("(3let _ be _/ in _)"
     1.9                          [0,0,60] 60)
    1.10  
    1.11 -  "_letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    1.12 +  "_letrec"  :: "[id,id,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    1.13                          [0,0,0,60] 60)
    1.14  
    1.15 -  "_letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    1.16 +  "_letrec2" :: "[id,id,id,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    1.17                          [0,0,0,0,60] 60)
    1.18  
    1.19 -  "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    1.20 +  "_letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    1.21                          [0,0,0,0,0,60] 60)
    1.22  
    1.23  ML {*