removed obsolete dummy_pat_tr;
authorwenzelm
Fri, 07 Oct 2005 22:59:23 +0200
changeset 17785 8d928051d6a7
parent 17784 5cbb52f2c478
child 17786 f06d6498ebf0
removed obsolete dummy_pat_tr;
src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Fri Oct 07 22:59:22 2005 +0200
+++ b/src/HOL/Bali/Basis.thy	Fri Oct 07 22:59:23 2005 +0200
@@ -352,16 +352,4 @@
 done 
 
 
-section "dummy pattern for quantifiers, let, etc."
-
-syntax
-  "@dummy_pat"   :: pttrn    ("'_")
-
-parse_translation {*
-let fun dummy_pat_tr [] = Free ("_",dummyT)
-  | dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts);
-in [("@dummy_pat", dummy_pat_tr)] 
 end
-*}
-
-end