src/HOL/thy_syntax.ML
changeset 6426 9a2ace82b68e
parent 6381 ed0c7b4a325d
child 6477 e36581d04eee
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Apr 14 14:42:53 1999 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Apr 14 14:44:04 1999 +0200
     1.3 @@ -42,19 +42,20 @@
     1.4  
     1.5  fun inductive_decl coind =
     1.6    let
     1.7 +    val no_atts = map (mk_pair o rpair "[]");
     1.8      fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
     1.9        if Syntax.is_identifier s then "op " ^ s else "_";
    1.10      fun mk_params (((recs, ipairs), monos), con_defs) =
    1.11        let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
    1.12            and srec_tms = mk_list recs
    1.13 -          and sintrs   = mk_big_list (map snd ipairs)
    1.14 +          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
    1.15        in
    1.16          ";\n\n\
    1.17          \local\n\
    1.18          \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
    1.19          \  InductivePackage.add_inductive true " ^
    1.20          (if coind then "true " else "false ") ^ srec_tms ^ " " ^
    1.21 -         sintrs ^ " " ^ mk_list monos ^ " " ^ mk_list con_defs ^ " thy;\n\
    1.22 +         sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
    1.23          \in\n\
    1.24          \structure " ^ big_rec_name ^ " =\n\
    1.25          \struct\n\