src/Pure/Thy/syntax.ML
changeset 201 9e41c6cec27c
parent 123 0a2f744e008a
child 257 b36874cf3b0b
equal deleted inserted replaced
200:39a931cc6558 201:9e41c6cec27c
   129 
   129 
   130 fun mk_simple_sext mfix =
   130 fun mk_simple_sext mfix =
   131   "Some (Syntax.simple_sext\n   " ^ mfix ^ ")";
   131   "Some (Syntax.simple_sext\n   " ^ mfix ^ ")";
   132 
   132 
   133 fun mk_ext ((cl, def, ty, ar, co, ax), sext) =
   133 fun mk_ext ((cl, def, ty, ar, co, ax), sext) =
   134   " (" ^ space_implode ",\n  " [cl, def, ty, ar, co, sext] ^ ")\n " ^ ax ^ "\n";
   134   " (" ^ space_implode ",\n  " [cl, def, ty, "[]",ar, co, sext] ^ ")\n " ^ ax ^ "\n";
   135 
   135 
   136 fun mk_ext_thy (base, name, ext, sext) =
   136 fun mk_ext_thy (base, name, ext, sext) =
   137   "extend_theory (" ^ base ^ ")\n " ^ quote name ^ "\n" ^ mk_ext (ext, sext);
   137   "extend_theory (" ^ base ^ ")\n " ^ quote name ^ "\n" ^ mk_ext (ext, sext);
   138 
   138 
   139 val preamble =
   139 val preamble =