tuned;
authorwenzelm
Mon Jun 01 10:47:08 2015 +0200 (2015-06-01)
changeset 60324f83406084507
parent 60323 9b3b812e6957
child 60325 6fc771cb42eb
tuned;
src/Pure/more_thm.ML
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/more_thm.ML	Sun May 31 00:20:35 2015 +0200
     1.2 +++ b/src/Pure/more_thm.ML	Mon Jun 01 10:47:08 2015 +0200
     1.3 @@ -279,10 +279,9 @@
     1.4    fun init _ : T = (Termtab.empty, true);
     1.5  );
     1.6  
     1.7 -fun declare_hyps ct ctxt =
     1.8 -  if Theory.subthy (Thm.theory_of_cterm ct, Proof_Context.theory_of ctxt) then
     1.9 -    (Hyps.map o apfst) (Termtab.update (Thm.term_of ct, ())) ctxt
    1.10 -  else raise CTERM ("assume_hyps: bad background theory", [ct]);
    1.11 +fun declare_hyps raw_ct ctxt =
    1.12 +  let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct
    1.13 +  in (Hyps.map o apfst) (Termtab.update (Thm.term_of ct, ())) ctxt end;
    1.14  
    1.15  fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
    1.16  
     2.1 --- a/src/Pure/raw_simplifier.ML	Sun May 31 00:20:35 2015 +0200
     2.2 +++ b/src/Pure/raw_simplifier.ML	Mon Jun 01 10:47:08 2015 +0200
     2.3 @@ -1295,11 +1295,10 @@
     2.4    let
     2.5      val thy = Proof_Context.theory_of raw_ctxt;
     2.6  
     2.7 -    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
     2.8 +    val ct = raw_ct
     2.9 +      |> Thm.transfer_cterm thy
    2.10 +      |> Thm.adjust_maxidx_cterm ~1;
    2.11      val maxidx = Thm.maxidx_of_cterm ct;
    2.12 -    val _ =
    2.13 -      Theory.subthy (Thm.theory_of_cterm ct, thy) orelse
    2.14 -        raise CTERM ("rewrite_cterm: bad background theory", [ct]);
    2.15  
    2.16      val ctxt =
    2.17        raw_ctxt