src/HOL/Tools/Predicate_Compile/core_data.ML
changeset 61424 c3658c18b7bc
parent 60752 b48830b670a1
child 61845 c5c7bc41185c
     1.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4      val thy = Proof_Context.theory_of ctxt
     1.5      val nargs = length (binder_types (fastype_of pred))
     1.6      fun meta_eq_of th = th RS @{thm eq_reflection}
     1.7 -    val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
     1.8 +    val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}]
     1.9  
    1.10      fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) =
    1.11        let