# HG changeset patch
# User lcp
# Date 797158302 -7200
# Node ID 91d09e2627994629ff89ab67ef28ee0a5406d526
# Parent  a58082b8066cb445f818ca1c608c9dc65c3b9f67
Gave tighter priorities to if, napply and the let-forms to
reduce ambiguities.

diff -r a58082b8066c -r 91d09e262799 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Thu Apr 06 10:49:53 1995 +0200
+++ b/src/CCL/Term.thy	Thu Apr 06 10:51:42 1995 +0200
@@ -11,38 +11,45 @@
 
 consts
 
-  one        ::	      "i"
+  one        :: "i"
 
-  if         ::       "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [] 60)
+  if         :: "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
 
-  inl,inr    ::	      "i=>i"
-  when       ::	      "[i,i=>i,i=>i]=>i" 
+  inl,inr    :: "i=>i"
+  when       :: "[i,i=>i,i=>i]=>i" 
 
-  split      ::	      "[i,[i,i]=>i]=>i"
+  split      :: "[i,[i,i]=>i]=>i"
   fst,snd,   
-  thd        ::       "i=>i"
+  thd        :: "i=>i"
 
-  zero       ::	      "i"
-  succ       ::	      "i=>i"
-  ncase      ::	      "[i,i,i=>i]=>i"
-  nrec       ::	      "[i,i,[i,i]=>i]=>i"
+  zero       :: "i"
+  succ       :: "i=>i"
+  ncase      :: "[i,i,i=>i]=>i"
+  nrec       :: "[i,i,[i,i]=>i]=>i"
 
-  nil        ::       "i"                    ("([])")
-  "$"        ::       "[i,i]=>i"             (infixr 80)
-  lcase      ::	      "[i,i,[i,i]=>i]=>i"
-  lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
+  nil        :: "i"                        ("([])")
+  "$"        :: "[i,i]=>i"                 (infixr 80)
+  lcase      :: "[i,i,[i,i]=>i]=>i"
+  lrec       :: "[i,i,[i,i,i]=>i]=>i"
+
+  let        :: "[i,i=>i]=>i"
+  letrec     :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
+  letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
+  letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
 
-  let        ::       "[i,i=>i]=>i"
-  letrec     ::       "[[i,i=>i]=>i,(i=>i)=>i]=>i"
-  letrec2    ::       "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
-  letrec3    ::       "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
+  "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
+  			[0,0,60] 60)
+
+  "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
+  			[0,0,0,60] 60)
 
-  "@let"     ::       "[idt,i,i]=>i"             ("(3let _ be _/ in _)" [] 60)
-  "@letrec"  ::       "[idt,idt,i,i]=>i"          ("(3letrec _ _ be _/ in _)"  [] 60)
-  "@letrec2" ::       "[idt,idt,idt,i,i]=>i"       ("(3letrec _ _ _ be _/ in _)"  [] 60)
-  "@letrec3" ::       "[idt,idt,idt,idt,i,i]=>i"    ("(3letrec _ _ _ _ be _/ in _)"  [] 60)
+  "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
+  			[0,0,0,0,60] 60)
 
-  napply    :: "[i=>i,i,i]=>i"      ("(_ ^ _ ` _)")
+  "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
+  			[0,0,0,0,0,60] 60)
+
+  napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
 
 rules