--- 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);