added constdefs
authorclasohm
Wed Mar 06 14:11:41 1996 +0100 (1996-03-06)
changeset 1555a5f48457dfd5
parent 1554 4ee99a973be4
child 1556 2fd82cec17d4
added constdefs
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Mar 06 14:10:44 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Mar 06 14:11:41 1996 +0100
     1.3 @@ -351,6 +351,22 @@
     1.4  val axiom_decls = repeat1 (ident -- !! string) >> mk_axiom_decls;
     1.5  
     1.6  
     1.7 +(* combined consts and axioms *)
     1.8 +
     1.9 +fun mk_constaxiom_decls x =
    1.10 +  let
    1.11 +    val (axms_defs, axms_names) =
    1.12 +      mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
    1.13 +  in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
    1.14 +       "\n\n|> add_defs\n" ^ axms_defs, axms_names)
    1.15 +  end;
    1.16 +
    1.17 +val constaxiom_decls =
    1.18 +  repeat1 (ident --$$ "::" -- !!
    1.19 +           ((string || const_type false >> quote) -- opt_mixfix) -- !!
    1.20 +           string) >> mk_constaxiom_decls;
    1.21 +
    1.22 +
    1.23  (* axclass *)
    1.24  
    1.25  fun mk_axclass_decl ((c, cs), axms) =
    1.26 @@ -516,6 +532,7 @@
    1.27    section "MLtext" "" verbatim,
    1.28    axm_section "rules" "|> add_axioms" axiom_decls,
    1.29    axm_section "defs" "|> add_defs" axiom_decls,
    1.30 +  axm_section "constdefs" "|> add_consts" constaxiom_decls,
    1.31    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.32    section "instance" "" instance_decl];
    1.33