changeset 17785 | 8d928051d6a7 |
parent 16417 | 9bc16273c2d4 |
child 17876 | b9c92f384109 |
--- 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