tuned;

--- a/src/Pure/more_thm.ML	Sun May 31 00:20:35 2015 +0200
+++ b/src/Pure/more_thm.ML	Mon Jun 01 10:47:08 2015 +0200
@@ -279,10 +279,9 @@
   fun init _ : T = (Termtab.empty, true);
 );
 
-fun declare_hyps ct ctxt =
-  if Theory.subthy (Thm.theory_of_cterm ct, Proof_Context.theory_of ctxt) then
-    (Hyps.map o apfst) (Termtab.update (Thm.term_of ct, ())) ctxt
-  else raise CTERM ("assume_hyps: bad background theory", [ct]);
+fun declare_hyps raw_ct ctxt =
+  let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct
+  in (Hyps.map o apfst) (Termtab.update (Thm.term_of ct, ())) ctxt end;
 
 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
 

--- a/src/Pure/raw_simplifier.ML	Sun May 31 00:20:35 2015 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon Jun 01 10:47:08 2015 +0200
@@ -1295,11 +1295,10 @@
   let
     val thy = Proof_Context.theory_of raw_ctxt;
 
-    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
+    val ct = raw_ct
+      |> Thm.transfer_cterm thy
+      |> Thm.adjust_maxidx_cterm ~1;
     val maxidx = Thm.maxidx_of_cterm ct;
-    val _ =
-      Theory.subthy (Thm.theory_of_cterm ct, thy) orelse
-        raise CTERM ("rewrite_cterm: bad background theory", [ct]);
 
     val ctxt =
       raw_ctxt