Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/pure_thy.ML
changeset 17703 6ec36bad47ea
parent 17496 26535df536ae
child 17930 e7160d70be1f 
--- a/src/Pure/pure_thy.ML	Thu Sep 29 00:58:55 2005 +0200
+++ b/src/Pure/pure_thy.ML	Thu Sep 29 00:58:56 2005 +0200
@@ -509,7 +509,8 @@
     [Const ("==", [aT, aT] ---> propT),
      Const ("==>", [propT, propT] ---> propT),
      Const ("all", (aT --> propT) --> propT),
-     Const ("TYPE", a_itselfT)]
+     Const ("TYPE", a_itselfT),
+     Const (Term.dummy_patternN, aT)]
   |> Theory.add_modesyntax ("", false)
     (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   |> Theory.add_trfuns Syntax.pure_trfuns
isabelle