changeset 59621 | 291934bac95e |
parent 59582 | 0fbed69ff081 |
child 60826 | 695cf1fab6cc |
--- a/src/Pure/Proof/proof_syntax.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 06 15:58:56 2015 +0100 @@ -197,7 +197,7 @@ |> add_proof_atom_consts (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); in - (Thm.cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) + (Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) end; fun read_term thy topsort =