# HG changeset patch
# User wenzelm
# Date 1003247527 -7200
# Node ID d69e7acd9380e38dce1c9e025fae6593e840475d
# Parent  30f2104953a154e8280461fcb87e0d84eb5e2688
TypedefPackage.add_typedef_no_result;

diff -r 30f2104953a1 -r d69e7acd9380 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Tue Oct 16 17:51:50 2001 +0200
+++ b/src/HOL/thy_syntax.ML	Tue Oct 16 17:52:07 2001 +0200
@@ -280,7 +280,7 @@
 val _ = ThySyn.add_syntax
  ["intrs", "monos", "con_defs", "congs", "simpset", "|",
   "and", "distinct", "inject", "induct"]
- [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
+ [axm_section "typedef" "|> TypedefPackage.add_typedef_no_result" typedef_decl,
   section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
   section "inductive" 	"" (inductive_decl false),
   section "coinductive"	"" (inductive_decl true),