--- a/src/HOL/Tools/hologic.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/hologic.ML Sun Jul 05 15:02:30 2015 +0200
@@ -207,14 +207,14 @@
let
val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
- val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
+ val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
fun conj_elim ctxt thPQ =
let
val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
- val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
+ val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
in (thP, thQ) end;