# HG changeset patch # User wenzelm # Date 1117696658 -7200 # Node ID a5c77d298ad7358d444f68d3ad002260ef8fa847 # Parent 22324687e2d2506f60e34d12eee1eb3d0d211168 swap declaration of thm/axm names to accomodate change in name space treatment; diff -r 22324687e2d2 -r a5c77d298ad7 src/Pure/Proof/proof_syntax.ML --- 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;