# HG changeset patch
# User wenzelm
# Date 1128718763 -7200
# Node ID 8d928051d6a7d8f02d14b4740bd0e8f7671c7ce9
# Parent  5cbb52f2c478baa5bef24d932582f215000e4be2
removed obsolete dummy_pat_tr;

diff -r 5cbb52f2c478 -r 8d928051d6a7 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