removed obsolete dummy_pat_tr;
authorwenzelm
Fri Oct 07 22:59:23 2005 +0200 (2005-10-07)
changeset 177858d928051d6a7
parent 17784 5cbb52f2c478
child 17786 f06d6498ebf0
removed obsolete dummy_pat_tr;
src/HOL/Bali/Basis.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Fri Oct 07 22:59:22 2005 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Fri Oct 07 22:59:23 2005 +0200
     1.3 @@ -352,16 +352,4 @@
     1.4  done 
     1.5  
     1.6  
     1.7 -section "dummy pattern for quantifiers, let, etc."
     1.8 -
     1.9 -syntax
    1.10 -  "@dummy_pat"   :: pttrn    ("'_")
    1.11 -
    1.12 -parse_translation {*
    1.13 -let fun dummy_pat_tr [] = Free ("_",dummyT)
    1.14 -  | dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts);
    1.15 -in [("@dummy_pat", dummy_pat_tr)] 
    1.16  end
    1.17 -*}
    1.18 -
    1.19 -end