src/HOL/Tools/rewrite_hol_proof.ML
changeset 33388 d64545e6cba5
parent 32010 cb1a1c94b4cd
child 33722 e588744f14da
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 20:48:08 2009 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 20:50:48 2009 +0100
     1.3 @@ -15,8 +15,8 @@
     1.4  
     1.5  open Proofterm;
     1.6  
     1.7 -val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
     1.8 -    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
     1.9 +val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
    1.10 +    Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
    1.11  
    1.12    (** eliminate meta-equality rules **)
    1.13