# HG changeset patch
# User wenzelm
# Date 1433015557 -7200
# Node ID c08adefc98ea3d5bba958c603f84cbb8206e2490
# Parent  6e465f0d46d3270f25c717941561992c1fbde287
more explicit context;

diff -r 6e465f0d46d3 -r c08adefc98ea src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat May 30 21:28:01 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat May 30 21:52:37 2015 +0200
@@ -81,7 +81,7 @@
     val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
   in
     ((Drule.implies_elim_list thm' (map Thm.assume prems)
-        |> Drule.implies_intr_list (map Drule.norm_hhf_cterm As)
+        |> Drule.implies_intr_list (map (Drule.norm_hhf_cterm ctxt') As)
         |> Drule.forall_intr_list xs)
       COMP rule)
     |> Drule.implies_intr_list prems
diff -r 6e465f0d46d3 -r c08adefc98ea src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat May 30 21:28:01 2015 +0200
+++ b/src/Pure/drule.ML	Sat May 30 21:52:37 2015 +0200
@@ -81,7 +81,7 @@
   val norm_hhf_eqs: thm list
   val is_norm_hhf: term -> bool
   val norm_hhf: theory -> term -> term
-  val norm_hhf_cterm: cterm -> cterm
+  val norm_hhf_cterm: Proof.context -> cterm -> cterm
   val protect: cterm -> cterm
   val protectI: thm
   val protectD: thm
@@ -706,9 +706,12 @@
   if is_norm_hhf t then t
   else Pattern.rewrite_term thy [norm_hhf_prop] [] t;
 
-fun norm_hhf_cterm ct =
-  if is_norm_hhf (Thm.term_of ct) then ct
-  else cterm_fun (Pattern.rewrite_term (Thm.theory_of_cterm ct) [norm_hhf_prop] []) ct;
+fun norm_hhf_cterm ctxt raw_ct =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val ct = Thm.transfer_cterm thy raw_ct;
+    val t = Thm.term_of ct;
+  in if is_norm_hhf t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end;
 
 
 (* var indexes *)
diff -r 6e465f0d46d3 -r c08adefc98ea src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat May 30 21:28:01 2015 +0200
+++ b/src/Pure/thm.ML	Sat May 30 21:52:37 2015 +0200
@@ -34,6 +34,7 @@
   val maxidx_of_cterm: cterm -> int
   val global_cterm_of: theory -> term -> cterm
   val cterm_of: Proof.context -> term -> cterm
+  val transfer_cterm: theory -> cterm -> cterm
   val renamed_term: term -> cterm -> cterm
   val dest_comb: cterm -> cterm * cterm
   val dest_fun: cterm -> cterm
@@ -196,13 +197,24 @@
 
 val cterm_of = global_cterm_of o Proof_Context.theory_of;
 
+fun merge_thys0 (Cterm {thy = thy1, ...}) (Cterm {thy = thy2, ...}) =
+  Theory.merge (thy1, thy2);
+
+fun transfer_cterm thy' ct =
+  let
+    val Cterm {thy, t, T, maxidx, sorts} = ct;
+    val _ =
+      Theory.subthy (thy, thy') orelse
+        raise CTERM ("transfer_cterm: not a super theory", [ct]);
+  in
+    if Theory.eq_thy (thy, thy') then ct
+    else Cterm {thy = thy', t = t, T = T, maxidx = maxidx, sorts = sorts}
+  end;
+
 fun renamed_term t' (Cterm {thy, t, T, maxidx, sorts}) =
   if t aconv t' then Cterm {thy = thy, t = t', T = T, maxidx = maxidx, sorts = sorts}
   else raise TERM ("renamed_term: terms disagree", [t, t']);
 
-fun merge_thys0 (Cterm {thy = thy1, ...}) (Cterm {thy = thy2, ...}) =
-  Theory.merge (thy1, thy2);
-
 
 (* destructors *)