Added []-field to extend_theory to accomodate type abbreviations.
authornipkow
Tue, 21 Dec 1993 16:27:36 +0100
changeset 201 9e41c6cec27c
parent 200 39a931cc6558
child 202 4e68398cdc06
Added []-field to extend_theory to accomodate type abbreviations.
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);