# HG changeset patch
# User wenzelm
# Date 941036945 -7200
# Node ID 7ad4dd78a9a7518a42e7c9155026d191a46d54c1
# Parent  61102e8cbe3c47e80639ac0995c427d097dc9d7d
dummy_pattern: aprop;

diff -r 61102e8cbe3c -r 7ad4dd78a9a7 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Oct 27 16:54:43 1999 +0200
+++ b/src/Pure/pure_thy.ML	Wed Oct 27 17:09:05 1999 +0200
@@ -428,7 +428,8 @@
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Theory.add_syntax
-   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
+   [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
+    (dummy_patternN, "aprop", Delimfix "'_")]
   |> Theory.add_consts
    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),