1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML Wed Jun 18 18:55:00 2008 +0200
1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Wed Jun 18 18:55:01 2008 +0200
1.3 @@ -17,7 +17,7 @@
1.4 open Proofterm;
1.5
1.6 val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
1.7 - Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
1.8 + Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
1.9
1.10 (** eliminate meta-equality rules **)
1.11