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/Provers/quantifier1.ML
changeset 36610 bafd82950e24
parent 35762 af3ff2ba4c54
child 38452 abc655166d61
child 38456 6769ccd90ad6 
--- a/src/Provers/quantifier1.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Provers/quantifier1.ML	Mon May 03 14:25:56 2010 +0200
@@ -113,7 +113,7 @@
   in exqu [] end;
 
 fun prove_conv tac thy tu =
-  Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
+  Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
     (K (rtac iff_reflection 1 THEN tac));
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
isabelle