src/HOL/Fun.thy
changeset 51717 9e7d1c139569
parent 51598 5dbe537087aa
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Fun.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -795,9 +795,10 @@
     1.4          | find t = NONE
     1.5      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
     1.6  
     1.7 -  fun proc ss ct =
     1.8 +  val ss = simpset_of @{context}
     1.9 +
    1.10 +  fun proc ctxt ct =
    1.11      let
    1.12 -      val ctxt = Simplifier.the_context ss
    1.13        val t = Thm.term_of ct
    1.14      in
    1.15        case find_double t of
    1.16 @@ -807,7 +808,7 @@
    1.17              (fn _ =>
    1.18                rtac eq_reflection 1 THEN
    1.19                rtac ext 1 THEN
    1.20 -              simp_tac (Simplifier.inherit_context ss @{simpset}) 1))
    1.21 +              simp_tac (put_simpset ss ctxt) 1))
    1.22      end
    1.23  in proc end
    1.24  *}