src/Pure/raw_simplifier.ML
changeset 62876 507c90523113
parent 61354 1727d7d14d76
child 62913 13252110a6fe
     1.1 --- a/src/Pure/raw_simplifier.ML	Tue Apr 05 19:41:58 2016 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Tue Apr 05 20:03:24 2016 +0200
     1.3 @@ -1392,11 +1392,10 @@
     1.4    Variable.gen_all ctxt;
     1.5  
     1.6  val hhf_ss =
     1.7 -  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
     1.8 -    addsimps Drule.norm_hhf_eqs);
     1.9 +  simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs);
    1.10  
    1.11  val hhf_protect_ss =
    1.12 -  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
    1.13 +  simpset_of (empty_simpset (Context.the_local_context ())
    1.14      addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong);
    1.15  
    1.16  in