src/Pure/raw_simplifier.ML
changeset 60324 f83406084507
parent 60184 7541f29492c3
child 60642 48dd1cefb4ae
     1.1 --- a/src/Pure/raw_simplifier.ML	Sun May 31 00:20:35 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon Jun 01 10:47:08 2015 +0200
     1.3 @@ -1295,11 +1295,10 @@
     1.4    let
     1.5      val thy = Proof_Context.theory_of raw_ctxt;
     1.6  
     1.7 -    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
     1.8 +    val ct = raw_ct
     1.9 +      |> Thm.transfer_cterm thy
    1.10 +      |> Thm.adjust_maxidx_cterm ~1;
    1.11      val maxidx = Thm.maxidx_of_cterm ct;
    1.12 -    val _ =
    1.13 -      Theory.subthy (Thm.theory_of_cterm ct, thy) orelse
    1.14 -        raise CTERM ("rewrite_cterm: bad background theory", [ct]);
    1.15  
    1.16      val ctxt =
    1.17        raw_ctxt