src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 51314 eac4bb5adbf9
parent 50056 72efd6b4038d
child 51552 c713c9505f68
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 28 16:38:17 2013 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 28 16:54:52 2013 +0100
     1.3 @@ -1158,15 +1158,11 @@
     1.4  
     1.5  (* preprocessing rules *)
     1.6  
     1.7 -fun Trueprop_conv cv ct =
     1.8 -  case Thm.term_of ct of
     1.9 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
    1.10 -  | _ => raise Fail "Trueprop_conv"
    1.11 -
    1.12  fun preprocess_equality thy rule =
    1.13    Conv.fconv_rule
    1.14      (imp_prems_conv
    1.15 -      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
    1.16 +      (HOLogic.Trueprop_conv
    1.17 +        (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
    1.18      (Thm.transfer thy rule)
    1.19  
    1.20  fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy