src/HOL/Tools/hologic.ML
changeset 35625 9c818cab0dd0
parent 35267 8dfd816713c6
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/hologic.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -190,14 +190,14 @@
     1.4  
     1.5  fun conj_intr thP thQ =
     1.6    let
     1.7 -    val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ)
     1.8 +    val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
     1.9        handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
    1.10      val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
    1.11    in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
    1.12  
    1.13  fun conj_elim thPQ =
    1.14    let
    1.15 -    val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ))
    1.16 +    val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
    1.17        handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
    1.18      val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
    1.19      val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;