src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 61424 c3658c18b7bc
parent 61268 abe08fb15a12
child 62581 fc5198b44314
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -884,9 +884,9 @@
     1.4      val intro'''' =
     1.5        Simplifier.full_simplify
     1.6          (put_simpset HOL_basic_ss ctxt
     1.7 -          addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
     1.8 +          addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}])
     1.9        intro'''
    1.10 -    (* splitting conjunctions introduced by Pair_eq*)
    1.11 +    (* splitting conjunctions introduced by prod.inject*)
    1.12      val intro''''' = split_conjuncts_in_assms ctxt intro''''
    1.13    in
    1.14      intro'''''