# HG changeset patch
# User wenzelm
# Date 1574961203 -3600
# Node ID 71467e35fc3ca64ab6e25cd3fb443a7f1907c470
# Parent  b4d409c65a769c6210dba0e057edad108ed22883
more structural integrity;

diff -r b4d409c65a76 -r 71467e35fc3c src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Nov 28 18:13:23 2019 +0100
@@ -314,6 +314,7 @@
       SOME (transform_function_data (inst_morph u) data) handle Pattern.MATCH => NONE
   in
     get_first match (retrieve_function_data ctxt t)
+    |> Option.map (transform_function_data (Morphism.transfer_morphism' ctxt))
   end
 
 fun import_last_function ctxt =
diff -r b4d409c65a76 -r 71467e35fc3c src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/Pure/assumption.ML	Thu Nov 28 18:13:23 2019 +0100
@@ -128,14 +128,10 @@
 
 (* export *)
 
-fun normalize ctxt0 th0 =
-  let val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0)
-  in Raw_Simplifier.norm_hhf_protect ctxt th end;
-
 fun export is_goal inner outer =
-  normalize inner #>
+  Raw_Simplifier.norm_hhf_protect inner #>
   fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
-  normalize outer;
+  Raw_Simplifier.norm_hhf_protect outer;
 
 fun export_term inner outer =
   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
diff -r b4d409c65a76 -r 71467e35fc3c src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/Pure/raw_simplifier.ML	Thu Nov 28 18:13:23 2019 +0100
@@ -1426,15 +1426,14 @@
 
 local
 
-fun gen_norm_hhf ss ctxt =
-  Thm.transfer' ctxt #>
-  (fn th =>
-    if Drule.is_norm_hhf (Thm.prop_of th) then th
-    else
-      Conv.fconv_rule
-        (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th) #>
-  Thm.adjust_maxidx_thm ~1 #>
-  Variable.gen_all ctxt;
+fun gen_norm_hhf ss ctxt0 th0 =
+  let
+    val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0);
+    val th' =
+      if Drule.is_norm_hhf (Thm.prop_of th) then th
+      else
+        Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th;
+  in th' |> Thm.adjust_maxidx_thm ~1 |> Variable.gen_all ctxt end;
 
 val hhf_ss =
   Context.the_local_context ()
diff -r b4d409c65a76 -r 71467e35fc3c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/Pure/thm.ML	Thu Nov 28 18:13:23 2019 +0100
@@ -610,9 +610,9 @@
   else transfer thy th;
 
 fun join_transfer_context (ctxt, th) =
-  if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then
-    (Context.raw_transfer (theory_of_thm th) ctxt, th)
-  else (ctxt, transfer' ctxt th);
+  if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt))
+  then (ctxt, transfer' ctxt th)
+  else (Context.raw_transfer (theory_of_thm th) ctxt, th);
 
 
 (* matching *)