src/HOL/thy_syntax.ML
changeset 12180 91c9f661b183
parent 12050 6934c005aec4
child 12505 46bfc675015a
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Nov 14 18:42:34 2001 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Nov 14 18:44:27 2001 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4      val no_atts = map (mk_pair o rpair "[]");
     1.5      fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
     1.6        if Syntax.is_identifier s then "op " ^ s else "_";
     1.7 -    fun mk_params (((recs, ipairs), monos), con_defs) =
     1.8 +    fun mk_params ((recs, ipairs), monos) =
     1.9        let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
    1.10            and srec_tms = mk_list recs
    1.11            and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
    1.12 @@ -64,7 +64,7 @@
    1.13          \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
    1.14          \  InductivePackage.add_inductive true " ^
    1.15          (if coind then "true " else "false ") ^ srec_tms ^
    1.16 -         sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
    1.17 +         sintrs ^ " " ^ mk_list (no_atts monos) ^ " thy;\n\
    1.18          \in\n\
    1.19          \structure " ^ big_rec_name ^ " =\n\
    1.20          \struct\n\
    1.21 @@ -83,10 +83,7 @@
    1.22        end
    1.23      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    1.24      fun optlist s = optional (s $$-- list1 name) []
    1.25 -  in
    1.26 -    repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs"
    1.27 -      >> mk_params
    1.28 -  end;
    1.29 +  in repeat1 name -- ipairs -- optlist "monos" >> mk_params end;
    1.30  
    1.31  
    1.32  
    1.33 @@ -278,8 +275,7 @@
    1.34  in
    1.35  
    1.36  val _ = ThySyn.add_syntax
    1.37 - ["intrs", "monos", "con_defs", "congs", "simpset", "|",
    1.38 -  "and", "distinct", "inject", "induct"]
    1.39 + ["intrs", "monos", "congs", "simpset", "|", "and", "distinct", "inject", "induct"]
    1.40   [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
    1.41    section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
    1.42    section "inductive" 	"" (inductive_decl false),