# HG changeset patch
# User traytel
# Date 1457293159 -3600
# Node ID b5d656bf0441ca643c70c6396d58a7477f0d3645
# Parent  347150095fd25aabab32df27ec33c0f2027db222
less resetting of local theories

diff -r 347150095fd2 -r b5d656bf0441 src/HOL/Library/bnf_axiomatization.ML
--- a/src/HOL/Library/bnf_axiomatization.ML	Sun Mar 06 10:33:34 2016 +0100
+++ b/src/HOL/Library/bnf_axiomatization.ML	Sun Mar 06 20:39:19 2016 +0100
@@ -81,9 +81,8 @@
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
 
-    val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
-      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
-      ||> `Local_Theory.reset;
+    val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
+      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
 
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
@@ -92,7 +91,7 @@
       |> Conjunction.elim_balanced (length wit_goals)
       |> map2 (Conjunction.elim_balanced o length) wit_goalss
       |> (map o map) (Thm.forall_elim_vars 0);
-    val phi = Proof_Context.export_morphism lthy_old lthy;
+    val phi = Local_Theory.target_morphism lthy;
     val thms = unflat all_goalss (Morphism.fact phi raw_thms);
 
     val (bnf, lthy') = after_qed mk_wit_thms thms lthy
diff -r 347150095fd2 -r b5d656bf0441 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Sun Mar 06 10:33:34 2016 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Sun Mar 06 20:39:19 2016 +0100
@@ -215,7 +215,6 @@
     |> snd
     |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
-    |> Local_Theory.reset
   end
 
 (* BNF interpretation *)
@@ -250,8 +249,8 @@
 fun fp_sugar_transfer_rules (fp_sugar:fp_sugar) =
   let
     val fp_ctr_sugar = #fp_ctr_sugar fp_sugar
-    val transfer_rules = #ctr_transfers fp_ctr_sugar @ #case_transfers fp_ctr_sugar 
-      @ #disc_transfers fp_ctr_sugar @ #sel_transfers fp_ctr_sugar 
+    val transfer_rules = #ctr_transfers fp_ctr_sugar @ #case_transfers fp_ctr_sugar
+      @ #disc_transfers fp_ctr_sugar @ #sel_transfers fp_ctr_sugar
       @ (#co_rec_transfers o #fp_co_induct_sugar) fp_sugar
     val transfer_attr = @{attributes [transfer_rule]}
   in
@@ -262,13 +261,12 @@
   let
     val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar)
     val type_name = type_name_of_bnf (#fp_bnf fp_sugar)
-    val pred_data = lookup_defined_pred_data lthy type_name 
+    val pred_data = lookup_defined_pred_data lthy type_name
       |> Transfer.update_pred_simps pred_injects
   in
-    lthy 
+    lthy
     |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
-    |> Local_Theory.reset
   end
 
 fun transfer_fp_sugars_interpretation fp_sugar lthy =