src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 38549 d0385f2764d8
parent 38072 7b8c295af291
child 38558 32ad17fe2b9c
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 10:27:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 11:02:14 2010 +0200
     1.3 @@ -524,7 +524,7 @@
     1.4  
     1.5  fun dest_conjunct_prem th =
     1.6    case HOLogic.dest_Trueprop (prop_of th) of
     1.7 -    (Const ("op &", _) $ t $ t') =>
     1.8 +    (Const (@{const_name "op &"}, _) $ t $ t') =>
     1.9        dest_conjunct_prem (th RS @{thm conjunct1})
    1.10          @ dest_conjunct_prem (th RS @{thm conjunct2})
    1.11      | _ => [th]
    1.12 @@ -576,7 +576,7 @@
    1.13  
    1.14  fun Trueprop_conv cv ct =
    1.15    case Thm.term_of ct of
    1.16 -    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
    1.17 +    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
    1.18    | _ => raise Fail "Trueprop_conv"
    1.19  
    1.20  fun preprocess_intro thy rule =
    1.21 @@ -587,7 +587,7 @@
    1.22  
    1.23  fun preprocess_elim ctxt elimrule =
    1.24    let
    1.25 -    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
    1.26 +    fun replace_eqs (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
    1.27         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
    1.28       | replace_eqs t = t
    1.29      val thy = ProofContext.theory_of ctxt