changeset 22675 | acf10be7dcca |
parent 21858 | 05f57309170c |
child 22796 | 34c316d7b630 |
--- a/src/Pure/Proof/proof_syntax.ML Sat Apr 14 11:05:12 2007 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sat Apr 14 17:35:52 2007 +0200 @@ -236,9 +236,7 @@ |> add_proof_syntax |> add_proof_atom_consts (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) - in - fn T => fn s => Thm.term_of (read_cterm thy' (s, T)) - end; + in Sign.simple_read_term thy' end; fun read_proof thy = let val rd = read_term thy proofT