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/Decision_Procs/cooper_tac.ML
changeset 60325 6fc771cb42eb
parent 59629 0d77c51b5040
child 60754 02924903a6fd 
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Mon Jun 01 10:47:08 2015 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Mon Jun 01 11:46:03 2015 +0200
@@ -85,7 +85,7 @@
       (case Thm.prop_of pre_thm of
         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
           let
-            val pth = linzqe_oracle (Thm.cterm_of ctxt (Envir.eta_long [] t1))
+            val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1)
           in
             ((pth RS iffD2) RS pre_thm,
               assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
isabelle