swap declaration of thm/axm names to accomodate change in name space
treatment;

--- a/src/Pure/Proof/proof_syntax.ML	Thu Jun 02 09:12:56 2005 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Thu Jun 02 09:17:38 2005 +0200
@@ -223,7 +223,7 @@
     val sg = sign_of thy |>
       add_proof_syntax |>
       add_proof_atom_consts
-        (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
+        (map (add_prefix "axm") axm_names @ map (add_prefix "thm") thm_names)
   in
     (cterm_of sg (term_of_proof prf'),
      proof_of_term thy tab true o Thm.term_of)
@@ -237,7 +237,7 @@
     val sg = sign_of thy |>
       add_proof_syntax |>
       add_proof_atom_consts
-        (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
+        (map (add_prefix "axm") axm_names @ map (add_prefix "thm") thm_names)
   in
     (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   end;