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/Library/Old_SMT/old_z3_proof_methods.ML
changeset 59498 50b60f501b05
parent 59058 a78612c67ec0
child 59586 ddf6deaadfe8 
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -72,7 +72,7 @@
   in
     Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
     |> apply (rtac @{thm injI})
-    |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
+    |> apply (Tactic.solve_tac ctxt' [rule, rule RS @{thm sym}])
     |> Goal.norm_result ctxt' o Goal.finish ctxt'
     |> singleton (Variable.export ctxt' ctxt)
   end
isabelle