src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 56245 84fc7dfa3cd4
parent 56239 17df7145a871
child 56254 a2dd9200854d
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -460,14 +460,14 @@
     1.4  
     1.5  (* general syntactic functions *)
     1.6  
     1.7 -fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
     1.8 +fun is_equationlike_term (Const (@{const_name Pure.eq}, _) $ _ $ _) = true
     1.9    | is_equationlike_term
    1.10        (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
    1.11    | is_equationlike_term _ = false
    1.12  
    1.13  val is_equationlike = is_equationlike_term o prop_of
    1.14  
    1.15 -fun is_pred_equation_term (Const ("==", _) $ u $ v) =
    1.16 +fun is_pred_equation_term (Const (@{const_name Pure.eq}, _) $ u $ v) =
    1.17        (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
    1.18    | is_pred_equation_term _ = false
    1.19  
    1.20 @@ -620,7 +620,7 @@
    1.21  (*
    1.22  fun equals_conv lhs_cv rhs_cv ct =
    1.23    case Thm.term_of ct of
    1.24 -    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
    1.25 +    Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.arg_conv cv ct
    1.26    | _ => error "equals_conv"
    1.27  *)
    1.28  
    1.29 @@ -973,7 +973,8 @@
    1.30  
    1.31  fun imp_prems_conv cv ct =
    1.32    (case Thm.term_of ct of
    1.33 -    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
    1.34 +    Const (@{const_name Pure.imp}, _) $ _ $ _ =>
    1.35 +      Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
    1.36    | _ => Conv.all_conv ct)
    1.37  
    1.38