routine check of theory context;
authorwenzelm
Mon Aug 31 18:59:27 2015 +0200 (2015-08-31)
changeset 613541727d7d14d76
parent 61353 b7e822883535
child 61355 31829cf53f5d
routine check of theory context;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Tue Oct 06 21:12:01 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon Aug 31 18:59:27 2015 +0200
     1.3 @@ -1381,13 +1381,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_norm_hhf ss ctxt th =
     1.8 -  (if Drule.is_norm_hhf (Thm.prop_of th) then th
     1.9 -   else
    1.10 -    Conv.fconv_rule
    1.11 -      (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
    1.12 -  |> Thm.adjust_maxidx_thm ~1
    1.13 -  |> Variable.gen_all ctxt;
    1.14 +fun gen_norm_hhf ss ctxt =
    1.15 +  Thm.transfer (Proof_Context.theory_of ctxt) #>
    1.16 +  (fn th =>
    1.17 +    if Drule.is_norm_hhf (Thm.prop_of th) then th
    1.18 +    else
    1.19 +      Conv.fconv_rule
    1.20 +        (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th) #>
    1.21 +  Thm.adjust_maxidx_thm ~1 #>
    1.22 +  Variable.gen_all ctxt;
    1.23  
    1.24  val hhf_ss =
    1.25    simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))