src/HOL/Tools/rewrite_hol_proof.ML
changeset 32010 cb1a1c94b4cd
parent 30850 5e20f9c20086
child 33388 d64545e6cba5
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Jul 15 23:48:21 2009 +0200
@@ -15,8 +15,8 @@
 
 open Proofterm;
 
-val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
-    Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
+val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
+    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
 
   (** eliminate meta-equality rules **)