src/Pure/pure_thy.ML

   |> Theory.add_modesyntax (Symbol.symbolsN, true) Syntax.pure_sym_syntax
   |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
   |> 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)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),