src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 51717 9e7d1c139569
parent 51552 c713c9505f68
child 52230 1105b3b5aa77
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -873,8 +873,10 @@
     1.4      val t_insts' = map rewrite_pat t_insts
     1.5      val intro'' = Thm.instantiate (T_insts, t_insts') intro
     1.6      val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     1.7 -    val intro'''' = Simplifier.full_simplify
     1.8 -      (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
     1.9 +    val intro'''' =
    1.10 +      Simplifier.full_simplify
    1.11 +        (put_simpset HOL_basic_ss ctxt
    1.12 +          addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
    1.13        intro'''
    1.14      (* splitting conjunctions introduced by Pair_eq*)
    1.15      val intro''''' = split_conjuncts_in_assms ctxt intro''''