adapted AxClass.add_axclass;
authorwenzelm
Wed Mar 17 13:42:42 1999 +0100 (1999-03-17)
changeset 63785780d71203bb
parent 6377 e7b051fae849
child 6379 2b17ff28a6cc
adapted AxClass.add_axclass;
PureThy.get_thm axioms;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Mar 17 13:41:50 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Mar 17 13:42:42 1999 +0100
     1.3 @@ -363,6 +363,7 @@
     1.4  (* axioms *)
     1.5  
     1.6  val mk_axms = mk_big_list o map (mk_pair o apfst quote);
     1.7 +val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst quote);
     1.8  
     1.9  fun mk_axiom_decls axms = (mk_axms axms, map fst axms);
    1.10  
    1.11 @@ -392,8 +393,8 @@
    1.12  (* axclass *)
    1.13  
    1.14  fun mk_axclass_decl ((c, cs), axms) =
    1.15 -  (mk_pair (c, cs) ^ "\n" ^ mk_axms axms,
    1.16 -    (strip_quotes c ^ "I") :: map fst axms);
    1.17 +  (mk_pair (c, cs) ^ "\n" ^ mk_axms' axms,
    1.18 +    strip_quotes c ^ "I" :: map fst axms);
    1.19  
    1.20  val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl;
    1.21  
    1.22 @@ -534,7 +535,7 @@
    1.23  
    1.24  (* standard sections *)
    1.25  
    1.26 -fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";";
    1.27 +fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ quote ax ^ ";";
    1.28  val mk_vals = cat_lines o map mk_val;
    1.29  
    1.30  fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)
    1.31 @@ -565,7 +566,7 @@
    1.32    axm_section "defs" "|> (PureThy.add_defs o map Thm.no_attributes)" axiom_decls,
    1.33    section "oracle" "|> Theory.add_oracle" oracle_decl,
    1.34    axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    1.35 -  axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.36 +  axm_section "axclass" "|> (#1 ooo AxClass.add_axclass)" axclass_decl,
    1.37    section "instance" "" instance_decl,
    1.38    section "path" "|> Theory.add_path" name,
    1.39    section "global" "|> PureThy.global_path" empty_decl,