# HG changeset patch
# User paulson
# Date 1441309200 -3600
# Node ID 44baf4d5e375fbed4ba3a30cbb747ef6d6808a01
# Parent  3c2d4636cebcf91b3c27d7b2c74384af2fbdcbf3# Parent  8ed21464e260b4ca128e3e35a7a419d3a3031cc8
merged

diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -808,10 +808,6 @@
           end
       end;
 
-    fun maybe_restore lthy_old lthy =
-      lthy |> not (Context.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
-        ? Local_Theory.restore;
-
     val map_bind_def =
       (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
          map_rhs);
@@ -830,10 +826,11 @@
       (bnf_set_terms, raw_set_defs)),
       (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) =
         no_defs_lthy
+        |> Local_Theory.open_target |> snd
         |> maybe_define true map_bind_def
         ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
         ||>> maybe_define true bd_bind_def
-        ||> `(maybe_restore no_defs_lthy);
+        ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -929,9 +926,10 @@
 
     val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> maybe_define (is_some rel_rhs_opt) rel_bind_def
       ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs
-      ||> `(maybe_restore lthy);
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bnf_rel_def = Morphism.thm phi raw_rel_def;
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -1219,8 +1219,9 @@
       #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
 
     val ((cst, (_, def)), (lthy', lthy)) = lthy0
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy lthy';
 
@@ -2135,10 +2136,11 @@
           #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed;
 
         val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
+          |> Local_Theory.open_target |> snd
           |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
               Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
             ctr_bindings ctr_mixfixes ctr_rhss
-          ||> `Local_Theory.restore;
+          ||> `Local_Theory.close_target;
 
         val phi = Proof_Context.export_morphism lthy lthy';
 
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -396,8 +396,9 @@
       resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
       |>> map_prod rev rev;
     val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
+      |> Local_Theory.open_target |> snd
       |> mk_recs
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism raw_lthy lthy;
 
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -303,8 +303,9 @@
 
     val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
@@ -382,8 +383,9 @@
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
@@ -530,8 +532,9 @@
 
     val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
@@ -653,10 +656,11 @@
 
     val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> fold_map (fn i => Local_Theory.define
         ((lsbis_bind i, NoSyn), (lsbis_def_bind i, lsbis_spec i))) ks
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -738,8 +742,9 @@
 
           val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
             lthy
+            |> Local_Theory.open_target |> snd
             |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
-            ||> `Local_Theory.restore;
+            ||> `Local_Theory.close_target;
 
           val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -836,11 +841,12 @@
 
     val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define
         ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
         ks xs isNode_setss
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -875,10 +881,11 @@
 
     val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> fold_map (fn i =>
         Local_Theory.define ((carT_bind i, NoSyn), (carT_def_bind i, carT_spec i))) ks
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -907,11 +914,12 @@
 
     val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define
         ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
         ks tree_maps treeFTs
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -976,8 +984,9 @@
 
     val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -1019,8 +1028,9 @@
 
     val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -1061,10 +1071,11 @@
 
     val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 2} (fn i => fn z =>
         Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -1336,12 +1347,13 @@
 
     val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
         Local_Theory.define ((dtor_bind i, NoSyn),
           (dtor_def_bind i, dtor_spec rep str mapx Jz Jz')))
         ks Rep_Ts str_finals map_FTs Jzs Jzs'
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     fun mk_dtors passive =
@@ -1381,12 +1393,13 @@
 
     val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 4} (fn i => fn abs => fn f => fn z =>
         Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
           ks Abs_Ts (map (fn i => HOLogic.mk_comp
             (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val unfolds = map (Morphism.term phi) unfold_frees;
@@ -1474,10 +1487,11 @@
 
     val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> fold_map (fn i =>
         Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec i))) ks
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     fun mk_ctors params =
@@ -1546,11 +1560,12 @@
 
     val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 3} (fn i => fn T => fn AT =>
         Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
           ks Ts activeAs
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val corecs = map (Morphism.term phi) corec_frees;
@@ -1742,11 +1757,12 @@
 
         val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) =
           lthy
+          |> Local_Theory.open_target |> snd
           |> @{fold_map 4} (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
             ((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec')))
             ls Zeros hrecs hrecs'
           |>> apsnd split_list o split_list
-          ||> `Local_Theory.restore;
+          ||> `Local_Theory.close_target;
 
         val phi = Proof_Context.export_morphism lthy_old lthy;
 
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -251,8 +251,9 @@
 
     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
@@ -331,8 +332,9 @@
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
@@ -472,8 +474,9 @@
 
           val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
             lthy
+            |> Local_Theory.open_target |> snd
             |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
-            ||> `Local_Theory.restore;
+            ||> `Local_Theory.close_target;
 
           val phi = Proof_Context.export_morphism lthy_old lthy;
 
@@ -656,10 +659,11 @@
 
     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> fold_map (fn i => Local_Theory.define
         ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
@@ -768,10 +772,11 @@
 
     val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> fold_map (fn i => Local_Theory.define
         ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val str_inits =
@@ -926,12 +931,13 @@
 
     val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 4} (fn i => fn abs => fn str => fn mapx =>
         Local_Theory.define
           ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx)))
           ks Abs_Ts str_inits map_FT_inits
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     fun mk_ctors passive =
@@ -978,10 +984,11 @@
 
     val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> fold_map (fn i =>
         Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val folds = map (Morphism.term phi) fold_frees;
@@ -1086,10 +1093,11 @@
 
     val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> fold_map (fn i =>
         Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     fun mk_dtors params =
@@ -1157,10 +1165,11 @@
 
     val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> @{fold_map 3} (fn i => fn T => fn AT =>
         Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
       |>> apsnd split_list o split_list
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val recs = map (Morphism.term phi) rec_frees;
@@ -1417,8 +1426,9 @@
 
               val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) =
                 lthy
+                |> Local_Theory.open_target |> snd
                 |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec))
-                ||> `Local_Theory.restore;
+                ||> `Local_Theory.close_target;
 
               val phi = Proof_Context.export_morphism lthy_old lthy;
 
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -183,14 +183,15 @@
       val nested_size_gen_o_maps_complete = forall (not o null) nested_size_gen_o_mapss;
       val nested_size_gen_o_maps = fold (union Thm.eq_thm_prop) nested_size_gen_o_mapss [];
 
-      val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
+      val ((raw_size_consts, raw_size_defs), (lthy1, lthy1_old)) = lthy0
+        |> Local_Theory.open_target |> snd
         |> apfst split_list o @{fold_map 2} (fn b => fn rhs =>
             Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
             #>> apsnd snd)
           size_bs size_rhss
-        ||> `Local_Theory.restore;
+        ||> `Local_Theory.close_target;
 
-      val phi = Proof_Context.export_morphism lthy1 lthy1';
+      val phi = Proof_Context.export_morphism lthy1_old lthy1;
 
       val size_defs = map (Morphism.thm phi) raw_size_defs;
 
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -145,10 +145,9 @@
     val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Proof_Context.concealed
+      |> Local_Theory.open_target |> snd
       |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
-      ||> Proof_Context.restore_naming lthy
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
     ((name, Typedef.transform_info phi info), lthy)
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -503,12 +503,13 @@
       (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
          Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss)));
 
-    val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
+    val ((raw_case, (_, raw_case_def)), (lthy, lthy_old)) = no_defs_lthy
+      |> Local_Theory.open_target |> snd
       |> Local_Theory.define ((case_binding, NoSyn),
         ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs))
-      ||> `Local_Theory.restore;
+      ||> `Local_Theory.close_target;
 
-    val phi = Proof_Context.export_morphism lthy lthy';
+    val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val case_def = Morphism.thm phi raw_case_def;
 
@@ -549,9 +550,9 @@
       forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso
       null sel_default_eqs;
 
-    val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
+    val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy) =
       if no_discs_sels then
-        (true, [], [], [], [], [], lthy')
+        (true, [], [], [], [], [], lthy)
       else
         let
           val all_sel_bindings = flat sel_bindingss;
@@ -623,6 +624,7 @@
 
           val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
             lthy
+            |> Local_Theory.open_target |> snd
             |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b =>
                 if Binding.is_empty b then
                   if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
@@ -636,7 +638,7 @@
             ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
               Specification.definition (SOME (b, NONE, NoSyn),
                 ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
-            ||> `Local_Theory.restore;
+            ||> `Local_Theory.close_target;
 
           val phi = Proof_Context.export_morphism lthy lthy';
 
@@ -1122,7 +1124,7 @@
         (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar)
       end;
   in
-    (goalss, after_qed, lthy')
+    (goalss, after_qed, lthy)
   end;
 
 fun free_constructors kind tacss = (fn (goalss, after_qed, lthy) =>
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Tools/typedef.ML	Thu Sep 03 20:40:00 2015 +0100
@@ -65,10 +65,15 @@
   fun merge data = Symtab.merge_list (K true) data;
 );
 
-val get_info = Symtab.lookup_list o Data.get o Context.Proof;
-val get_info_global = Symtab.lookup_list o Data.get o Context.Theory;
+fun get_info_generic context =
+  Symtab.lookup_list (Data.get context) #>
+  map (transform_info (Morphism.transfer_morphism (Context.theory_of context)));
 
-fun put_info name info = Data.map (Symtab.cons_list (name, info));
+val get_info = get_info_generic o Context.Proof;
+val get_info_global = get_info_generic o Context.Theory;
+
+fun put_info name info =
+  Data.map (Symtab.cons_list (name, transform_info Morphism.trim_context_morphism info));
 
 
 (* global interpretation *)
@@ -289,4 +294,3 @@
     >> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));
 
 end;
-
diff -r 3c2d4636cebc -r 44baf4d5e375 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/HOL/Typedef.thy	Thu Sep 03 20:40:00 2015 +0100
@@ -13,12 +13,11 @@
   fixes Rep and Abs and A
   assumes Rep: "Rep x \<in> A"
     and Rep_inverse: "Abs (Rep x) = x"
-    and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
+    and Abs_inverse: "y \<in> A \<Longrightarrow> Rep (Abs y) = y"
   -- \<open>This will be axiomatized for each typedef!\<close>
 begin
 
-lemma Rep_inject:
-  "(Rep x = Rep y) = (x = y)"
+lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y"
 proof
   assume "Rep x = Rep y"
   then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
@@ -27,44 +26,44 @@
   ultimately show "x = y" by simp
 next
   assume "x = y"
-  thus "Rep x = Rep y" by (simp only:)
+  then show "Rep x = Rep y" by (simp only:)
 qed
 
 lemma Abs_inject:
-  assumes x: "x \<in> A" and y: "y \<in> A"
-  shows "(Abs x = Abs y) = (x = y)"
+  assumes "x \<in> A" and "y \<in> A"
+  shows "Abs x = Abs y \<longleftrightarrow> x = y"
 proof
   assume "Abs x = Abs y"
   then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
-  moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)
-  moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
+  moreover from \<open>x \<in> A\<close> have "Rep (Abs x) = x" by (rule Abs_inverse)
+  moreover from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)
   ultimately show "x = y" by simp
 next
   assume "x = y"
-  thus "Abs x = Abs y" by (simp only:)
+  then show "Abs x = Abs y" by (simp only:)
 qed
 
 lemma Rep_cases [cases set]:
-  assumes y: "y \<in> A"
-    and hyp: "!!x. y = Rep x ==> P"
+  assumes "y \<in> A"
+    and hyp: "\<And>x. y = Rep x \<Longrightarrow> P"
   shows P
 proof (rule hyp)
-  from y have "Rep (Abs y) = y" by (rule Abs_inverse)
-  thus "y = Rep (Abs y)" ..
+  from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)
+  then show "y = Rep (Abs y)" ..
 qed
 
 lemma Abs_cases [cases type]:
-  assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
+  assumes r: "\<And>y. x = Abs y \<Longrightarrow> y \<in> A \<Longrightarrow> P"
   shows P
 proof (rule r)
   have "Abs (Rep x) = x" by (rule Rep_inverse)
-  thus "x = Abs (Rep x)" ..
+  then show "x = Abs (Rep x)" ..
   show "Rep x \<in> A" by (rule Rep)
 qed
 
 lemma Rep_induct [induct set]:
   assumes y: "y \<in> A"
-    and hyp: "!!x. P (Rep x)"
+    and hyp: "\<And>x. P (Rep x)"
   shows "P y"
 proof -
   have "P (Rep (Abs y))" by (rule hyp)
@@ -73,7 +72,7 @@
 qed
 
 lemma Abs_induct [induct type]:
-  assumes r: "!!y. y \<in> A ==> P (Abs y)"
+  assumes r: "\<And>y. y \<in> A \<Longrightarrow> P (Abs y)"
   shows "P x"
 proof -
   have "Rep x \<in> A" by (rule Rep)
@@ -84,25 +83,24 @@
 
 lemma Rep_range: "range Rep = A"
 proof
-  show "range Rep <= A" using Rep by (auto simp add: image_def)
-  show "A <= range Rep"
+  show "range Rep \<subseteq> A" using Rep by (auto simp add: image_def)
+  show "A \<subseteq> range Rep"
   proof
-    fix x assume "x : A"
-    hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
-    thus "x : range Rep" by (rule range_eqI)
+    fix x assume "x \<in> A"
+    then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
+    then show "x \<in> range Rep" by (rule range_eqI)
   qed
 qed
 
 lemma Abs_image: "Abs ` A = UNIV"
 proof
-  show "Abs ` A <= UNIV" by (rule subset_UNIV)
-next
-  show "UNIV <= Abs ` A"
+  show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
+  show "UNIV \<subseteq> Abs ` A"
   proof
     fix x
     have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
-    moreover have "Rep x : A" by (rule Rep)
-    ultimately show "x : Abs ` A" by (rule image_eqI)
+    moreover have "Rep x \<in> A" by (rule Rep)
+    ultimately show "x \<in> Abs ` A" by (rule image_eqI)
   qed
 qed
 
diff -r 3c2d4636cebc -r 44baf4d5e375 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/Pure/General/completion.scala	Thu Sep 03 20:40:00 2015 +0100
@@ -135,6 +135,10 @@
 
   /** semantic completion **/
 
+  def clean_name(s: String): Option[String] =
+    if (s == "" || s == "_") None
+    else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
+
   def report_no_completion(pos: Position.T): String =
     YXML.string_of_tree(Semantic.Info(pos, No_Completion))
 
diff -r 3c2d4636cebc -r 44baf4d5e375 src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Sep 03 20:27:53 2015 +0100
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Sep 03 20:40:00 2015 +0100
@@ -79,12 +79,16 @@
   {
     for {
       Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
+      name1 <- Completion.clean_name(name)
+
       original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
-      orig = Library.perhaps_unquote(original)
-      entries = complete(name).filter(_ != orig)
+      original1 <- Completion.clean_name(Library.perhaps_unquote(original))
+
+      entries = complete(name1).filter(_ != original1)
       if entries.nonEmpty
+
       items =
-        entries.map({
+        entries.sorted.map({
           case entry =>
             val full_name = Long_Name.qualify(Markup.CITATION, entry)
             val description = List(entry, "(BibTeX entry)")