Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/rewrite_hol_proof.ML
changeset 35845 e5980f0ad025
parent 33722 e588744f14da
child 36042 85efdadee8ae 
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -16,7 +16,7 @@
 open Proofterm;
 
 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)
+    Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
 
   (** eliminate meta-equality rules **)
isabelle