# HG changeset patch
# User nipkow
# Date 756487656 -3600
# Node ID 9e41c6cec27c1eacaf728802ef8e1e33fd3962fa
# Parent  39a931cc6558aa0f6b2160ee90dab4a18847036b
Added []-field to extend_theory to accomodate type abbreviations.

diff -r 39a931cc6558 -r 9e41c6cec27c src/Pure/Thy/syntax.ML
--- a/src/Pure/Thy/syntax.ML	Tue Dec 21 16:26:40 1993 +0100
+++ b/src/Pure/Thy/syntax.ML	Tue Dec 21 16:27:36 1993 +0100
@@ -131,7 +131,7 @@
   "Some (Syntax.simple_sext\n   " ^ mfix ^ ")";
 
 fun mk_ext ((cl, def, ty, ar, co, ax), sext) =
-  " (" ^ space_implode ",\n  " [cl, def, ty, ar, co, sext] ^ ")\n " ^ ax ^ "\n";
+  " (" ^ space_implode ",\n  " [cl, def, ty, "[]",ar, co, sext] ^ ")\n " ^ ax ^ "\n";
 
 fun mk_ext_thy (base, name, ext, sext) =
   "extend_theory (" ^ base ^ ")\n " ^ quote name ^ "\n" ^ mk_ext (ext, sext);