Changed structure of name spaces for datatypes.
authorberghofe
Fri Oct 16 18:50:20 1998 +0200 (1998-10-16)
changeset 5658082debccf486
parent 5657 1a6c9c6a3f8e
child 5659 e2a2be6089b4
Changed structure of name spaces for datatypes.
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Oct 16 17:36:12 1998 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Oct 16 18:50:20 1998 +0200
     1.3 @@ -113,12 +113,11 @@
     1.4            (if length names > 1 then
     1.5               "structure " ^ (space_implode "_" names) ^ " =\n\
     1.6               \struct\n\
     1.7 -             \val induct = induction;\n\
     1.8 -             \val recs = rec_thms;\n\
     1.9 -             \val simps = simps;\n\
    1.10 -             \val size = size;\n"
    1.11 -           else "") ^ structs ^
    1.12 -          (if length names > 1 then "end;\n" else "")
    1.13 +             \  val induct = induction;\n\
    1.14 +             \  val recs = rec_thms;\n\
    1.15 +             \  val simps = simps;\n\
    1.16 +             \  val size = size;\nend;\n"
    1.17 +           else "") ^ structs
    1.18          end);
    1.19  
    1.20    fun mk_dt_string dts =
    1.21 @@ -135,7 +134,7 @@
    1.22        ";\nlocal\n\
    1.23        \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
    1.24        \  case_thms, split_thms, induction, size, simps}) =\n\
    1.25 -      \  DatatypePackage.add_datatype " ^ add_datatype_args ^ " thy;\n\
    1.26 +      \  DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
    1.27        \in\n" ^ mk_bind_thms_string names ^
    1.28        "val thy = thy;\nend;\nval thy = thy\n"
    1.29      end;
    1.30 @@ -169,7 +168,7 @@
    1.31    val opt_typs = repeat ((string >> strip_quotes) ||
    1.32      simple_typ || ("(" $$-- complex_typ --$$ ")"));
    1.33    val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
    1.34 -    parens (n ^ ", " ^ mx ^ ", " ^ brackets (commas (map quote Ts))));
    1.35 +    parens (n ^ ", " ^ brackets (commas (map quote Ts)) ^ ", " ^ mx));
    1.36    val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
    1.37  
    1.38  in