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 42361 23f352990944
parent 38457 b8760b6e7c65
child 42456 13b4b6ba3593 
--- a/src/Provers/quantifier1.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/Provers/quantifier1.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -113,7 +113,7 @@
   in exqu [] end;
 
 fun prove_conv tac thy tu =
-  let val ctxt = ProofContext.init_global thy;
+  let val ctxt = Proof_Context.init_global thy;
       val eq_tu = Logic.mk_equals tu;
       val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
       val thm = Goal.prove ctxt' [] [] fixed_goal
isabelle