Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
allow syntax types within abbreviations;
authorwenzelm
Fri, 16 Apr 2010 20:56:40 +0200
changeset 36175 5cec4ca719d1
parent 36174 feb6f24de47e
child 36176 3fe7e97ccca8
allow syntax types within abbreviations;
src/Pure/Isar/typedecl.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/typedecl.ML	Fri Apr 16 20:17:38 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Fri Apr 16 20:56:40 2010 +0200
@@ -94,8 +94,8 @@
     |> pair name
   end;
 
-val abbrev = gen_abbrev ProofContext.cert_typ;
-val abbrev_cmd = gen_abbrev ProofContext.read_typ;
+val abbrev = gen_abbrev ProofContext.cert_typ_syntax;
+val abbrev_cmd = gen_abbrev ProofContext.read_typ_syntax;
 
 fun abbrev_global decl rhs =
   Theory_Target.init NONE
isabelle