diff -r acea2f336721 -r d64545e6cba5 src/Pure/Proof/extraction.ML
--- 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;