src/Pure/Proof/proof_syntax.ML

       map fst (Symtab.dest tab);
     val axm_names = map fst (List.concat (map (Symtab.dest o #axioms o rep_theory) thys));
     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)
   end;
 

     val thm_names = filter_out (equal "") (map fst (List.concat (map thms_of thys)));
     val axm_names = map fst (List.concat (map (Symtab.dest o #axioms o rep_theory) thys));
     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;
 
 fun read_proof thy =