# HG changeset patch
# User wenzelm
# Date 921674562 -3600
# Node ID 5780d71203bbef65dced1ae27717a95506830d3f
# Parent  e7b051fae84945295cef8933d32bd8794d561f10
adapted AxClass.add_axclass;
PureThy.get_thm axioms;

diff -r e7b051fae849 -r 5780d71203bb src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Mar 17 13:41:50 1999 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Wed Mar 17 13:42:42 1999 +0100
@@ -363,6 +363,7 @@
 (* axioms *)
 
 val mk_axms = mk_big_list o map (mk_pair o apfst quote);
+val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst quote);
 
 fun mk_axiom_decls axms = (mk_axms axms, map fst axms);
 
@@ -392,8 +393,8 @@
 (* axclass *)
 
 fun mk_axclass_decl ((c, cs), axms) =
-  (mk_pair (c, cs) ^ "\n" ^ mk_axms axms,
-    (strip_quotes c ^ "I") :: map fst axms);
+  (mk_pair (c, cs) ^ "\n" ^ mk_axms' axms,
+    strip_quotes c ^ "I" :: map fst axms);
 
 val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl;
 
@@ -534,7 +535,7 @@
 
 (* standard sections *)
 
-fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";";
+fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ quote ax ^ ";";
 val mk_vals = cat_lines o map mk_val;
 
 fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)
@@ -565,7 +566,7 @@
   axm_section "defs" "|> (PureThy.add_defs o map Thm.no_attributes)" axiom_decls,
   section "oracle" "|> Theory.add_oracle" oracle_decl,
   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
-  axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
+  axm_section "axclass" "|> (#1 ooo AxClass.add_axclass)" axclass_decl,
   section "instance" "" instance_decl,
   section "path" "|> Theory.add_path" name,
   section "global" "|> PureThy.global_path" empty_decl,