changeset 33388 | d64545e6cba5 |
parent 33337 | 9c3b9bf81e8b |
child 33522 | 737589bb9bb8 |
--- a/src/Pure/Proof/extraction.ML Mon Nov 02 20:48:08 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Mon Nov 02 20:50:48 2009 +0100 @@ -300,7 +300,7 @@ val rtypes = map fst types; val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); val thy' = add_syntax thy; - val rd = ProofSyntax.read_proof thy' false + val rd = Proof_Syntax.read_proof thy' false; in fn (thm, (vs, s1, s2)) => let val name = Thm.get_name thm;