# HG changeset patch
# User wenzelm
# Date 1271444200 -7200
# Node ID 5cec4ca719d1525dffec4d96298b0bde970a35be
# Parent  feb6f24de47e03c4cb297b283a4199e5b605d451
allow syntax types within abbreviations;

diff -r feb6f24de47e -r 5cec4ca719d1 src/Pure/Isar/typedecl.ML
--- 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