--- a/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 02 20:48:08 2009 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 02 20:50:48 2009 +0100
@@ -15,8 +15,8 @@
open Proofterm;
-val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
- Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
+val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
+ Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
(** eliminate meta-equality rules **)