# HG changeset patch
# User wenzelm
# Date 1441397814 -7200
# Node ID 4b5872b9d7832f0a0c46a346893eb7d162ea8175
# Parent  279a5b4f47bd10707aa4504c300167670162803e# Parent  6189d179c2b515fe90a81b908868797019089732
merged

diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -15,27 +15,27 @@
       Rep_bottom_iff: thm, Abs_bottom_iff: thm }
 
   val add_podef: binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> (Proof.context -> tactic) -> theory ->
+    term -> Typedef.bindings option -> (Proof.context -> tactic) -> theory ->
     (Typedef.info * thm) * theory
   val add_cpodef: binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
+    term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
     theory -> (Typedef.info * cpo_info) * theory
   val add_pcpodef: binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
+    term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
     theory -> (Typedef.info * cpo_info * pcpo_info) * theory
 
   val cpodef_proof:
     (binding * (string * sort) list * mixfix) * term
-    * (binding * binding) option -> theory -> Proof.state
+    * Typedef.bindings option -> theory -> Proof.state
   val cpodef_proof_cmd:
     (binding * (string * string option) list * mixfix) * string
-    * (binding * binding) option -> theory -> Proof.state
+    * Typedef.bindings option -> theory -> Proof.state
   val pcpodef_proof:
     (binding * (string * sort) list * mixfix) * term
-    * (binding * binding) option -> theory -> Proof.state
+    * Typedef.bindings option -> theory -> Proof.state
   val pcpodef_proof_cmd:
     (binding * (string * string option) list * mixfix) * string
-    * (binding * binding) option -> theory -> Proof.state
+    * Typedef.bindings option -> theory -> Proof.state
 end
 
 structure Cpodef : CPODEF =
@@ -63,13 +63,14 @@
 fun prove_cpo
       (name: binding)
       (newT: typ)
-      (Rep_name: binding, Abs_name: binding)
+      opt_bindings
       (type_definition: thm)  (* type_definition Rep Abs A *)
       (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
       (admissible: thm)       (* adm (%x. x : set) *)
       (thy: theory)
     =
   let
+    val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings;
     val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
     val (full_tname, Ts) = dest_Type newT
     val lhs_sorts = map (snd o dest_TFree) Ts
@@ -102,13 +103,14 @@
 fun prove_pcpo
       (name: binding)
       (newT: typ)
-      (Rep_name: binding, Abs_name: binding)
+      opt_bindings
       (type_definition: thm)  (* type_definition Rep Abs A *)
       (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
       (bottom_mem: thm)       (* bottom : set *)
       (thy: theory)
     =
   let
+    val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings;
     val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
     val (full_tname, Ts) = dest_Type newT
     val lhs_sorts = map (snd o dest_TFree) Ts
@@ -138,7 +140,7 @@
 
 (* prepare_cpodef *)
 
-fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
+fun prepare prep_term name (tname, raw_args, _) raw_set thy =
   let
     (*rhs*)
     val tmp_ctxt =
@@ -155,18 +157,15 @@
     val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args
     val full_tname = Sign.full_name thy tname
     val newT = Type (full_tname, map TFree lhs_tfrees)
-
-    val morphs = opt_morphs
-      |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
   in
-    (newT, oldT, set, morphs)
+    (newT, oldT, set)
   end
 
-fun add_podef typ set opt_morphs tac thy =
+fun add_podef typ set opt_bindings tac thy =
   let
     val name = #1 typ
     val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
-      |> Typedef.add_typedef_global false typ set opt_morphs tac
+      |> Typedef.add_typedef_global typ set opt_bindings tac
     val oldT = #rep_type (#1 info)
     val newT = #abs_type (#1 info)
     val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
@@ -189,13 +188,12 @@
       (prep_term: Proof.context -> 'a -> term)
       (typ: binding * (string * sort) list * mixfix)
       (raw_set: 'a)
-      (opt_morphs: (binding * binding) option)
+      opt_bindings
       (thy: theory)
     : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
   let
     val name = #1 typ
-    val (newT, oldT, set, morphs) =
-      prepare prep_term name typ raw_set opt_morphs thy
+    val (newT, oldT, set) = prepare prep_term name typ raw_set thy
 
     val goal_nonempty =
       HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)))
@@ -205,9 +203,9 @@
     fun cpodef_result nonempty admissible thy =
       let
         val ((info as (_, {type_definition, ...}), below_def), thy) = thy
-          |> add_podef typ set opt_morphs (fn ctxt => resolve_tac ctxt [nonempty] 1)
+          |> add_podef typ set opt_bindings (fn ctxt => resolve_tac ctxt [nonempty] 1)
         val (cpo_info, thy) = thy
-          |> prove_cpo name newT morphs type_definition below_def admissible
+          |> prove_cpo name newT opt_bindings type_definition below_def admissible
       in
         ((info, cpo_info), thy)
       end
@@ -221,13 +219,12 @@
       (prep_term: Proof.context -> 'a -> term)
       (typ: binding * (string * sort) list * mixfix)
       (raw_set: 'a)
-      (opt_morphs: (binding * binding) option)
+      opt_bindings
       (thy: theory)
     : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
   let
     val name = #1 typ
-    val (newT, oldT, set, morphs) =
-      prepare prep_term name typ raw_set opt_morphs thy
+    val (newT, oldT, set) = prepare prep_term name typ raw_set thy
 
     val goal_bottom_mem =
       HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set))
@@ -239,11 +236,11 @@
       let
         fun tac ctxt = resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt [bottom_mem] 1
         val ((info as (_, {type_definition, ...}), below_def), thy) = thy
-          |> add_podef typ set opt_morphs tac
+          |> add_podef typ set opt_bindings tac
         val (cpo_info, thy) = thy
-          |> prove_cpo name newT morphs type_definition below_def admissible
+          |> prove_cpo name newT opt_bindings type_definition below_def admissible
         val (pcpo_info, thy) = thy
-          |> prove_pcpo name newT morphs type_definition below_def bottom_mem
+          |> prove_pcpo name newT opt_bindings type_definition below_def bottom_mem
       in
         ((info, cpo_info, pcpo_info), thy)
       end
@@ -256,10 +253,10 @@
 
 (* tactic interface *)
 
-fun add_cpodef typ set opt_morphs (tac1, tac2) thy =
+fun add_cpodef typ set opt_bindings (tac1, tac2) thy =
   let
     val (goal1, goal2, cpodef_result) =
-      prepare_cpodef Syntax.check_term typ set opt_morphs thy
+      prepare_cpodef Syntax.check_term typ set opt_bindings thy
     val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context)
       handle ERROR msg => cat_error msg
         ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
@@ -268,10 +265,10 @@
         ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set))
   in cpodef_result thm1 thm2 thy end
 
-fun add_pcpodef typ set opt_morphs (tac1, tac2) thy =
+fun add_pcpodef typ set opt_bindings (tac1, tac2) thy =
   let
     val (goal1, goal2, pcpodef_result) =
-      prepare_pcpodef Syntax.check_term typ set opt_morphs thy
+      prepare_pcpodef Syntax.check_term typ set opt_bindings thy
     val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context)
       handle ERROR msg => cat_error msg
         ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
@@ -286,23 +283,23 @@
 local
 
 fun gen_cpodef_proof prep_term prep_constraint
-    ((b, raw_args, mx), set, opt_morphs) thy =
+    ((b, raw_args, mx), set, opt_bindings) thy =
   let
     val ctxt = Proof_Context.init_global thy
     val args = map (apsnd (prep_constraint ctxt)) raw_args
     val (goal1, goal2, make_result) =
-      prepare_cpodef prep_term (b, args, mx) set opt_morphs thy
+      prepare_cpodef prep_term (b, args, mx) set opt_bindings thy
     fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "cpodef_proof"
   in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
 
 fun gen_pcpodef_proof prep_term prep_constraint
-    ((b, raw_args, mx), set, opt_morphs) thy =
+    ((b, raw_args, mx), set, opt_bindings) thy =
   let
     val ctxt = Proof_Context.init_global thy
     val args = map (apsnd (prep_constraint ctxt)) raw_args
     val (goal1, goal2, make_result) =
-      prepare_pcpodef prep_term (b, args, mx) set opt_morphs thy
+      prepare_pcpodef prep_term (b, args, mx) set opt_bindings thy
     fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "pcpodef_proof"
   in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
@@ -321,24 +318,30 @@
 
 (** outer syntax **)
 
-val typedef_proof_decl =
+local
+
+fun cpodef pcpo =
   (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
   (@{keyword "="} |-- Parse.term) --
   Scan.option
     (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
+  >> (fn ((((args, t), mx), A), morphs) =>
+      Toplevel.theory_to_proof
+        ((if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
+          ((t, args, mx), A, SOME (Typedef.make_morphisms t morphs))))
 
-fun mk_pcpodef_proof pcpo ((((args, t), mx), A), morphs) =
-  (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
-    ((t, args, mx), A, morphs)
+in
 
 val _ =
   Outer_Syntax.command @{command_keyword pcpodef}
     "HOLCF type definition (requires admissibility proof)"
-    (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
+    (cpodef true)
 
 val _ =
   Outer_Syntax.command @{command_keyword cpodef}
     "HOLCF type definition (requires admissibility proof)"
-    (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
+    (cpodef false)
 
 end
+
+end
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -18,11 +18,11 @@
     }
 
   val add_domaindef: binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> theory ->
+    term -> Typedef.bindings option -> theory ->
     (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
 
   val domaindef_cmd: (binding * (string * string option) list * mixfix) * string
-    * (binding * binding) option -> theory -> theory
+    * Typedef.bindings option -> theory -> theory
 end
 
 structure Domaindef : DOMAINDEF =
@@ -80,7 +80,7 @@
       (prep_term: Proof.context -> 'a -> term)
       (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
       (raw_defl: 'a)
-      (opt_morphs: (binding * binding) option)
+      (opt_bindings: Typedef.bindings option)
       (thy: theory)
     : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
   let
@@ -100,10 +100,6 @@
     val full_tname = Sign.full_name thy tname
     val newT = Type (full_tname, map TFree lhs_tfrees)
 
-    (*morphisms*)
-    val morphs = opt_morphs
-      |> the_default (Binding.prefix_name "Rep_" tname, Binding.prefix_name "Abs_" tname)
-
     (*set*)
     val set = @{term "defl_set :: udom defl => udom set"} $ defl
 
@@ -111,7 +107,7 @@
     fun tac1 ctxt = resolve_tac ctxt @{thms defl_set_bottom} 1
     fun tac2 ctxt = resolve_tac ctxt @{thms adm_defl_set} 1
     val ((info, cpo_info, pcpo_info), thy) = thy
-      |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2)
+      |> Cpodef.add_pcpodef typ set opt_bindings (tac1, tac2)
 
     (*definitions*)
     val Rep_const = Const (#Rep_name (#1 info), newT --> udomT)
@@ -187,8 +183,8 @@
   handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print tname)
 
-fun add_domaindef typ defl opt_morphs thy =
-  gen_add_domaindef Syntax.check_term typ defl opt_morphs thy
+fun add_domaindef typ defl opt_bindings thy =
+  gen_add_domaindef Syntax.check_term typ defl opt_bindings thy
 
 fun domaindef_cmd ((b, raw_args, mx), A, morphs) thy =
   let
@@ -199,17 +195,13 @@
 
 (** outer syntax **)
 
-val domaindef_decl =
-  (Parse.type_args_constrained -- Parse.binding) --
-  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
-  Scan.option
-    (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-
-fun mk_domaindef (((((args, t)), mx), A), morphs) =
-  domaindef_cmd ((t, args, mx), A, morphs)
-
 val _ =
   Outer_Syntax.command @{command_keyword domaindef} "HOLCF definition of domains from deflations"
-    (domaindef_decl >> (Toplevel.theory o mk_domaindef))
+    ((Parse.type_args_constrained -- Parse.binding) --
+      Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
+      Scan.option
+        (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) >>
+     (fn (((((args, t)), mx), A), morphs) =>
+      Toplevel.theory (domaindef_cmd ((t, args, mx), A, SOME (Typedef.make_morphisms t morphs)))));
 
 end
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Import/import_rule.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -218,9 +218,12 @@
       | _ => error "type_introduction: bad type definition theorem"
     val tfrees = Term.add_tfrees c []
     val tnames = sort_strings (map fst tfrees)
+    val typedef_bindings =
+      Typedef.make_morphisms (Binding.name tycname)
+        (SOME (Binding.name rep_name, Binding.name abs_name))
     val ((_, typedef_info), thy') =
-     Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
-       (SOME (Binding.name rep_name, Binding.name abs_name)) (fn ctxt => resolve_tac ctxt [th2] 1) thy
+     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
+       (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
     val aty = #abs_type (#1 typedef_info)
     val th = freezeT thy' (#type_definition (#2 typedef_info))
     val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -410,7 +410,10 @@
   possibly slow dictionary constructions.
 \<close>
 
-definition card_UNIV' :: "'a card_UNIV"
+context
+begin
+
+qualified definition card_UNIV' :: "'a card_UNIV"
 where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
 
 lemma CARD_code [code_unfold]:
@@ -421,7 +424,7 @@
   "card_UNIV' = card_UNIV"
 by(simp add: card_UNIV card_UNIV'_def)
 
-hide_const (open) card_UNIV'
+end
 
 lemma card_Compl:
   "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
@@ -430,7 +433,7 @@
 context fixes xs :: "'a :: finite_UNIV list"
 begin
 
-definition finite' :: "'a set \<Rightarrow> bool"
+qualified definition finite' :: "'a set \<Rightarrow> bool"
 where [simp, code del, code_abbrev]: "finite' = finite"
 
 lemma finite'_code [code]:
@@ -443,7 +446,7 @@
 context fixes xs :: "'a :: card_UNIV list"
 begin
 
-definition card' :: "'a set \<Rightarrow> nat" 
+qualified definition card' :: "'a set \<Rightarrow> nat" 
 where [simp, code del, code_abbrev]: "card' = card"
  
 lemma card'_code [code]:
@@ -452,7 +455,7 @@
 by(simp_all add: List.card_set card_Compl card_UNIV)
 
 
-definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
 where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
 
 lemma subset'_code [code]:
@@ -462,7 +465,7 @@
 by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
   (metis finite_compl finite_set rev_finite_subset)
 
-definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
 where [simp, code del, code_abbrev]: "eq_set = op ="
 
 lemma eq_set_code [code]:
@@ -538,7 +541,4 @@
   by eval
 end
 
-hide_const (open) card' finite' subset' eq_set
-
 end
-
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -40,6 +40,9 @@
 
 subsection \<open>Basic arithmetic\<close>
 
+context
+begin
+
 lemma [code, code del]:
   "(plus :: nat \<Rightarrow> _) = plus" ..
 
@@ -51,7 +54,7 @@
 
 text \<open>Bounded subtraction needs some auxiliary\<close>
 
-definition dup :: "nat \<Rightarrow> nat" where
+qualified definition dup :: "nat \<Rightarrow> nat" where
   "dup n = n + n"
 
 lemma dup_code [code]:
@@ -59,7 +62,7 @@
   "dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
   by (simp_all add: dup_def numeral_Bit0)
 
-definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
+qualified definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
   "sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
 
 lemma sub_code [code]:
@@ -139,6 +142,8 @@
   "divmod_nat 0 n = (0, 0)"
   by (simp_all add: prod_eq_iff nat_of_num_numeral)
 
+end
+
 
 subsection \<open>Conversions\<close>
 
@@ -155,7 +160,4 @@
   code_module Code_Binary_Nat \<rightharpoonup>
     (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
-hide_const (open) dup sub
-
 end
-
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -85,20 +85,23 @@
     and (OCaml) "Pervasives.sqrt"
 declare sqrt_def[code del]
 
-definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
+context
+begin
+
+qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
 
 lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
   unfolding real_exp_def ..
 
+end
+
 code_printing
-  constant real_exp \<rightharpoonup>
+  constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
     (SML) "Math.exp"
     and (OCaml) "Pervasives.exp"
-declare real_exp_def[code del]
+declare Code_Real_Approx_By_Float.real_exp_def[code del]
 declare exp_def[code del]
 
-hide_const (open) real_exp
-
 code_printing
   constant ln \<rightharpoonup>
     (SML) "Math.ln"
@@ -149,7 +152,10 @@
     (SML) "Real.fromInt"
     and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
 
-definition real_of_int :: "int \<Rightarrow> real" where
+context
+begin
+
+qualified definition real_of_int :: "int \<Rightarrow> real" where
   [code_abbrev]: "real_of_int = of_int"
 
 lemma [code]:
@@ -172,7 +178,7 @@
   "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
   by simp
 
-hide_const (open) real_of_int
+end
 
 code_printing
   constant Ratreal \<rightharpoonup> (SML)
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Countable.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -66,15 +66,17 @@
 
 subsection \<open>Automatically proving countability of old-style datatypes\<close>
 
-inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
+context
+begin
+
+qualified inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
   undefined: "finite_item undefined"
 | In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)"
 | In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)"
 | Leaf: "finite_item (Old_Datatype.Leaf a)"
 | Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)"
 
-function
-  nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
+qualified function nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
 where
   "nth_item 0 = undefined"
 | "nth_item (Suc n) =
@@ -97,7 +99,7 @@
 lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)"
 unfolding sum_encode_def by simp
 
-termination
+qualified termination
 by (relation "measure id")
   (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
     le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
@@ -193,7 +195,7 @@
       end)
 \<close>
 
-hide_const (open) finite_item nth_item
+end
 
 
 subsection \<open>Automatically proving countability of datatypes\<close>
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -275,10 +275,13 @@
   "fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"
 | "fold_impl fn e [] = e"
 
-definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
+context
+begin
+
+qualified definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
   where "fold f e al = fold_impl f e (DAList.impl_of al)"
 
-hide_const (open) fold
+end
 
 context comp_fun_commute
 begin
@@ -348,7 +351,10 @@
 
 end
 
-lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
+context
+begin
+
+private lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
   by auto
 
 lemma image_mset_Bag [code]:
@@ -368,7 +374,7 @@
   qed
 qed
 
-hide_const single_alist_entry
+end
 
 (* we cannot use (\<lambda>a n. op + (a * n)) for folding, since * is not defined
    in comm_monoid_add *)
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/Debug.thy
--- a/src/HOL/Library/Debug.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Debug.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -6,37 +6,40 @@
 imports Main
 begin
 
-definition trace :: "String.literal \<Rightarrow> unit" where
+context
+begin
+
+qualified definition trace :: "String.literal \<Rightarrow> unit" where
   [simp]: "trace s = ()"
 
-definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
+qualified definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
   [simp]: "tracing s = id"
 
 lemma [code]:
   "tracing s = (let u = trace s in id)"
   by simp
 
-definition flush :: "'a \<Rightarrow> unit" where
+qualified definition flush :: "'a \<Rightarrow> unit" where
   [simp]: "flush x = ()"
 
-definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
   [simp]: "flushing x = id"
 
 lemma [code, code_unfold]:
   "flushing x = (let u = flush x in id)"
   by simp
 
-definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+qualified definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   [simp]: "timing s f x = f x"
 
+end
+
 code_printing
-  constant trace \<rightharpoonup> (Eval) "Output.tracing"
-| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
-| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
+  constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
+| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
+| constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
 
 code_reserved Eval Output Timing
 
-hide_const (open) trace tracing flush flushing timing
-
 end
 
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Discrete.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -8,7 +8,10 @@
 
 subsection \<open>Discrete logarithm\<close>
 
-fun log :: "nat \<Rightarrow> nat"
+context
+begin
+
+qualified fun log :: "nat \<Rightarrow> nat"
   where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
 
 lemma log_zero [simp]: "log 0 = 0"
@@ -67,7 +70,7 @@
 
 subsection \<open>Discrete square root\<close>
 
-definition sqrt :: "nat \<Rightarrow> nat"
+qualified definition sqrt :: "nat \<Rightarrow> nat"
   where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
 
 lemma sqrt_aux:
@@ -173,7 +176,6 @@
 lemma sqrt_le: "sqrt n \<le> n"
   using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
 
-hide_const (open) log sqrt
-
 end
 
+end
\ No newline at end of file
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Dlist.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -46,61 +46,71 @@
 
 text \<open>Fundamental operations:\<close>
 
-definition empty :: "'a dlist" where
+context
+begin
+
+qualified definition empty :: "'a dlist" where
   "empty = Dlist []"
 
-definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
   "insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
 
-definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
   "remove x dxs = Dlist (remove1 x (list_of_dlist dxs))"
 
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
+qualified definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
   "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
 
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
   "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
 
+end
+
 
 text \<open>Derived operations:\<close>
 
-definition null :: "'a dlist \<Rightarrow> bool" where
+context
+begin
+
+qualified definition null :: "'a dlist \<Rightarrow> bool" where
   "null dxs = List.null (list_of_dlist dxs)"
 
-definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
+qualified definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
   "member dxs = List.member (list_of_dlist dxs)"
 
-definition length :: "'a dlist \<Rightarrow> nat" where
+qualified definition length :: "'a dlist \<Rightarrow> nat" where
   "length dxs = List.length (list_of_dlist dxs)"
 
-definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
   "fold f dxs = List.fold f (list_of_dlist dxs)"
 
-definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
   "foldr f dxs = List.foldr f (list_of_dlist dxs)"
 
+end
+
 
 subsection \<open>Executable version obeying invariant\<close>
 
 lemma list_of_dlist_empty [simp, code abstract]:
-  "list_of_dlist empty = []"
-  by (simp add: empty_def)
+  "list_of_dlist Dlist.empty = []"
+  by (simp add: Dlist.empty_def)
 
 lemma list_of_dlist_insert [simp, code abstract]:
-  "list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)"
-  by (simp add: insert_def)
+  "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
+  by (simp add: Dlist.insert_def)
 
 lemma list_of_dlist_remove [simp, code abstract]:
-  "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
-  by (simp add: remove_def)
+  "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
+  by (simp add: Dlist.remove_def)
 
 lemma list_of_dlist_map [simp, code abstract]:
-  "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
-  by (simp add: map_def)
+  "list_of_dlist (Dlist.map f dxs) = remdups (List.map f (list_of_dlist dxs))"
+  by (simp add: Dlist.map_def)
 
 lemma list_of_dlist_filter [simp, code abstract]:
-  "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
-  by (simp add: filter_def)
+  "list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)"
+  by (simp add: Dlist.filter_def)
 
 
 text \<open>Explicit executable conversion\<close>
@@ -134,28 +144,29 @@
 subsection \<open>Induction principle and case distinction\<close>
 
 lemma dlist_induct [case_names empty insert, induct type: dlist]:
-  assumes empty: "P empty"
-  assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)"
+  assumes empty: "P Dlist.empty"
+  assumes insrt: "\<And>x dxs. \<not> Dlist.member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (Dlist.insert x dxs)"
   shows "P dxs"
 proof (cases dxs)
   case (Abs_dlist xs)
-  then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id)
+  then have "distinct xs" and dxs: "dxs = Dlist xs"
+    by (simp_all add: Dlist_def distinct_remdups_id)
   from \<open>distinct xs\<close> have "P (Dlist xs)"
   proof (induct xs)
-    case Nil from empty show ?case by (simp add: empty_def)
+    case Nil from empty show ?case by (simp add: Dlist.empty_def)
   next
     case (Cons x xs)
-    then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
-      by (simp_all add: member_def List.member_def)
-    with insrt have "P (insert x (Dlist xs))" .
-    with Cons show ?case by (simp add: insert_def distinct_remdups_id)
+    then have "\<not> Dlist.member (Dlist xs) x" and "P (Dlist xs)"
+      by (simp_all add: Dlist.member_def List.member_def)
+    with insrt have "P (Dlist.insert x (Dlist xs))" .
+    with Cons show ?case by (simp add: Dlist.insert_def distinct_remdups_id)
   qed
   with dxs show "P dxs" by simp
 qed
 
 lemma dlist_case [cases type: dlist]:
-  obtains (empty) "dxs = empty"
-    | (insert) x dys where "\<not> member dys x" and "dxs = insert x dys"
+  obtains (empty) "dxs = Dlist.empty"
+    | (insert) x dys where "\<not> Dlist.member dys x" and "dxs = Dlist.insert x dys"
 proof (cases dxs)
   case (Abs_dlist xs)
   then have dxs: "dxs = Dlist xs" and distinct: "distinct xs"
@@ -163,13 +174,13 @@
   show thesis
   proof (cases xs)
     case Nil with dxs
-    have "dxs = empty" by (simp add: empty_def) 
+    have "dxs = Dlist.empty" by (simp add: Dlist.empty_def) 
     with empty show ?thesis .
   next
     case (Cons x xs)
-    with dxs distinct have "\<not> member (Dlist xs) x"
-      and "dxs = insert x (Dlist xs)"
-      by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
+    with dxs distinct have "\<not> Dlist.member (Dlist xs) x"
+      and "dxs = Dlist.insert x (Dlist xs)"
+      by (simp_all add: Dlist.member_def List.member_def Dlist.insert_def distinct_remdups_id)
     with insert show ?thesis .
   qed
 qed
@@ -178,14 +189,11 @@
 subsection \<open>Functorial structure\<close>
 
 functor map: map
-  by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
+  by (simp_all add: remdups_map_remdups fun_eq_iff dlist_eq_iff)
 
 
 subsection \<open>Quickcheck generators\<close>
 
-quickcheck_generator dlist predicate: distinct constructors: empty, insert
-
-
-hide_const (open) member fold foldr empty insert remove map filter null member length fold
+quickcheck_generator dlist predicate: distinct constructors: Dlist.empty, Dlist.insert
 
 end
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/IArray.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -13,36 +13,35 @@
 lists first. Arrays could be converted back into lists for printing if they
 were wrapped up in an additional constructor.\<close>
 
+context
+begin
+
 datatype 'a iarray = IArray "'a list"
 
-primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
+qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
 "list_of (IArray xs) = xs"
-hide_const (open) list_of
 
-definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
+qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
 [simp]: "of_fun f n = IArray (map f [0..<n])"
-hide_const (open) of_fun
 
-definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
 [simp]: "as !! n = IArray.list_of as ! n"
-hide_const (open) sub
 
-definition length :: "'a iarray \<Rightarrow> nat" where
+qualified definition length :: "'a iarray \<Rightarrow> nat" where
 [simp]: "length as = List.length (IArray.list_of as)"
-hide_const (open) length
 
-fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
 "all p (IArray as) = (ALL a : set as. p a)"
-hide_const (open) all
 
-fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
 "exists p (IArray as) = (EX a : set as. p a)"
-hide_const (open) exists
 
 lemma list_of_code [code]:
 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
 by (cases as) (simp add: map_nth)
 
+end
+
 
 subsection "Code Generation"
 
@@ -86,10 +85,13 @@
   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
   by (cases as, cases bs) (simp add: equal)
 
-primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
+context
+begin
+
+qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
   "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
 
-hide_const (open) tabulate
+end
 
 lemma [code]:
   "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
@@ -98,10 +100,13 @@
 code_printing
   constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
 
-primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
+context
+begin
+
+qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
   [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
 
-hide_const (open) sub'
+end
 
 lemma [code]:
   "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
@@ -114,10 +119,13 @@
 code_printing
   constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
 
-definition length' :: "'a iarray \<Rightarrow> integer" where
+context
+begin
+
+qualified definition length' :: "'a iarray \<Rightarrow> integer" where
   [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
 
-hide_const (open) length'
+end
 
 lemma [code]:
   "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri Sep 04 22:16:54 2015 +0200
@@ -314,10 +314,10 @@
 and x :: 'a
 begin
 
-fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
 where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
 
-fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
+qualified fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
 where "rtrancl_while_step (ws, Z) =
   (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
   in (new @ tl ws, set new \<union> Z))"
@@ -325,12 +325,12 @@
 definition rtrancl_while :: "('a list * 'a set) option"
 where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
 
-fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
 where "rtrancl_while_invariant (ws, Z) =
    (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
     Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
 
-lemma rtrancl_while_invariant: 
+qualified lemma rtrancl_while_invariant: 
   assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
   shows   "rtrancl_while_invariant (rtrancl_while_step st)"
 proof (cases st)
@@ -392,7 +392,4 @@
 
 end
 
-hide_const (open) rtrancl_while_test rtrancl_while_step rtrancl_while_invariant
-hide_fact (open) rtrancl_while_invariant
-
 end
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Library/bnf_axiomatization.ML
--- a/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -86,9 +86,10 @@
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
+      |> Thm.close_derivation
       |> Conjunction.elim_balanced (length wit_goals)
       |> map2 (Conjunction.elim_balanced o length) wit_goalss
-      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
+      |> (map o map) (Thm.forall_elim_vars 0);
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val thms = unflat all_goalss (Morphism.fact phi raw_thms);
 
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -582,7 +582,7 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
-          Typedef.add_typedef_global false
+          Typedef.add_typedef_global
             (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
             (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -1484,9 +1484,9 @@
               Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                 (fn {context = ctxt, prems = _} =>
                    mk_set_transfer_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map))
+              |> Thm.close_derivation
               |> Conjunction.elim_balanced (length goals)
               |> Proof_Context.export names_lthy lthy
-              |> map Thm.close_derivation
           end;
 
         val set_transfer = Lazy.lazy mk_set_transfer;
@@ -1566,9 +1566,10 @@
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
+        |> Thm.close_derivation
         |> Conjunction.elim_balanced (length wit_goals)
         |> map2 (Conjunction.elim_balanced o length) wit_goalss
-        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
+        |> (map o map) (Thm.forall_elim_vars 0);
   in
     map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
       goals (map (fn tac => fn {context = ctxt, prems = _} =>
@@ -1585,9 +1586,10 @@
     fun mk_triv_wit_thms tac set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
+        |> Thm.close_derivation
         |> Conjunction.elim_balanced (length wit_goals)
         |> map2 (Conjunction.elim_balanced o length) wit_goalss
-        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
+        |> (map o map) (Thm.forall_elim_vars 0);
     val (mk_wit_thms, nontriv_wit_goals) =
       (case triv_tac_opt of
         NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -680,9 +680,9 @@
           Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
             (fn {context = ctxt, prems = _} =>
                mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs)
+          |> Thm.close_derivation
           |> Conjunction.elim_balanced (length goals)
           |> Proof_Context.export names_lthy lthy
-          |> map Thm.close_derivation
         end;
 
       val (set_cases_thms, set_cases_attrss) =
@@ -785,9 +785,9 @@
              else
                Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                  (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
+               |> Thm.close_derivation
                |> Conjunction.elim_balanced (length goals)
-               |> Proof_Context.export names_lthy lthy
-               |> map Thm.close_derivation)
+               |> Proof_Context.export names_lthy lthy)
         end;
 
       val rel_sel_thms =
@@ -884,9 +884,9 @@
               Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                 (fn {context = ctxt, prems = _} =>
                    mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm)
+              |> Thm.close_derivation
               |> Conjunction.elim_balanced (length goals)
               |> Proof_Context.export names_lthy lthy
-              |> map Thm.close_derivation
           end;
 
       val disc_transfer_thms =
@@ -897,9 +897,9 @@
             Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
               (fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt (the_single rel_sel_thms)
                  (the_single exhaust_discs) (flat (flat distinct_discsss)))
+            |> Thm.close_derivation
             |> Conjunction.elim_balanced (length goals)
             |> Proof_Context.export names_lthy lthy
-            |> map Thm.close_derivation
         end;
 
       val map_disc_iff_thms =
@@ -921,9 +921,9 @@
             Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
               (fn {context = ctxt, prems = _} =>
                  mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms)
+            |> Thm.close_derivation
             |> Conjunction.elim_balanced (length goals)
             |> Proof_Context.export names_lthy lthy
-            |> map Thm.close_derivation
         end;
 
       val (map_sel_thmss, map_sel_thms) =
@@ -956,9 +956,9 @@
                  (fn {context = ctxt, prems = _} =>
                     mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms
                       (flat sel_thmss) live_nesting_map_id0s)
+               |> Thm.close_derivation
                |> Conjunction.elim_balanced (length goals)
-               |> Proof_Context.export names_lthy lthy
-               |> map Thm.close_derivation)
+               |> Proof_Context.export names_lthy lthy)
         end;
 
       val (set_sel_thmssss, set_sel_thms) =
@@ -1015,9 +1015,9 @@
                  (fn {context = ctxt, prems = _} =>
                     mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
                       (flat sel_thmss) set0_thms)
+               |> Thm.close_derivation
                |> Conjunction.elim_balanced (length goals)
-               |> Proof_Context.export names_lthy lthy
-               |> map Thm.close_derivation)
+               |> Proof_Context.export names_lthy lthy)
         end;
 
       val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
@@ -2256,9 +2256,9 @@
           (fn {context = ctxt, prems = _} =>
              mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) xsssss
                rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
+        |> Thm.close_derivation
         |> Conjunction.elim_balanced nn
         |> Proof_Context.export names_lthy lthy
-        |> map Thm.close_derivation
       end;
 
     fun derive_rec_o_map_thmss lthy recs rec_defs =
@@ -2408,9 +2408,9 @@
              mk_corec_transfer_tac ctxt (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs)
                type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
                live_nesting_rel_eqs (flat pgss) pss qssss gssss)
+        |> Thm.close_derivation
         |> Conjunction.elim_balanced (length goals)
         |> Proof_Context.export names_lthy lthy
-        |> map Thm.close_derivation
       end;
 
     fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -143,10 +143,20 @@
   let
     (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
     val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
+
+    val default_bindings = Typedef.default_bindings (Binding.concealed b');
+    val bindings =
+      (case opt_morphs of
+        NONE => default_bindings
+      | SOME (Rep_name, Abs_name) =>
+         {Rep_name = Binding.concealed Rep_name,
+          Abs_name = Binding.concealed Abs_name,
+          type_definition_name = #type_definition_name default_bindings});
+
     val ((name, info), (lthy, lthy_old)) =
       lthy
       |> Local_Theory.open_target |> snd
-      |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
+      |> Typedef.add_typedef (b', Ts, mx) set (SOME bindings) tac
       ||> `Local_Theory.close_target;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -1017,9 +1017,9 @@
                   Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                     (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Thm.cterm_of ctxt u)
                        exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms)
+                  |> Thm.close_derivation
                   |> Conjunction.elim_balanced (length goals)
                   |> Proof_Context.export names_lthy lthy
-                  |> map Thm.close_derivation
                 end;
             in
               (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -76,6 +76,7 @@
     fun proves goals = goals
       |> Logic.mk_conjunction_balanced
       |> prove
+      |> Thm.close_derivation
       |> Conjunction.elim_balanced (length goals)
       |> map Simpdata.mk_eq;
   in
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -273,8 +273,7 @@
     val cong = #case_cong (Old_Datatype_Data.the_info thy n)
       |> safe_mk_meta_eq
   in
-    Context.theory_map
-      (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
+    Context.theory_map (Function_Context_Tree.add_function_cong cong) thy
   end
 
 val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -282,7 +282,7 @@
 
 fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt)))
 
-val store_termination_rule = Data.map o @{apply 4(1)} o cons
+val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
 
 val get_functions = #2 o Data.get o Context.Proof
 fun add_function_data (info : info as {fs, termination, ...}) =
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Function/function_context_tree.ML
--- a/src/HOL/Tools/Function/function_context_tree.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -10,10 +10,8 @@
   type ctxt = (string * typ) list * thm list
   type ctx_tree
 
-  (* FIXME: This interface is a mess and needs to be cleaned up! *)
   val get_function_congs : Proof.context -> thm list
   val add_function_cong : thm -> Context.generic -> Context.generic
-  val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
 
   val cong_add: attribute
   val cong_del: attribute
@@ -53,14 +51,17 @@
   val merge = Thm.merge_thms
 );
 
-val get_function_congs = FunctionCongs.get o Context.Proof
-val map_function_congs = FunctionCongs.map
-val add_function_cong = FunctionCongs.map o Thm.add_thm
+fun get_function_congs ctxt =
+  FunctionCongs.get (Context.Proof ctxt)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+
+val add_function_cong = FunctionCongs.map o Thm.add_thm o Thm.trim_context;
+
 
 (* congruence rules *)
 
-val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
+val cong_add = Thm.declaration_attribute (add_function_cong o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (FunctionCongs.map o Thm.del_thm o safe_mk_meta_eq);
 
 
 type depgraph = int Int_Graph.T
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -7,29 +7,35 @@
 signature PARTIAL_FUNCTION =
 sig
   val init: string -> term -> term -> thm -> thm -> thm option -> declaration
-
   val mono_tac: Proof.context -> int -> tactic
-
   val add_partial_function: string -> (binding * typ option * mixfix) list ->
     Attrib.binding * term -> local_theory -> local_theory
-
   val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
     Attrib.binding * string -> local_theory -> local_theory
 end;
 
-
 structure Partial_Function: PARTIAL_FUNCTION =
 struct
 
 (*** Context Data ***)
 
-datatype setup_data = Setup_Data of 
+datatype setup_data = Setup_Data of
  {fixp: term,
   mono: term,
   fixp_eq: thm,
   fixp_induct: thm,
   fixp_induct_user: thm option};
 
+fun transform_setup_data phi (Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user}) =
+  let
+    val term = Morphism.term phi;
+    val thm = Morphism.thm phi;
+  in
+    Setup_Data
+     {fixp = term fixp, mono = term mono, fixp_eq = thm fixp_eq,
+      fixp_induct = thm fixp_induct, fixp_induct_user = Option.map thm fixp_induct_user}
+  end;
+
 structure Modes = Generic_Data
 (
   type T = setup_data Symtab.table;
@@ -40,17 +46,18 @@
 
 fun init mode fixp mono fixp_eq fixp_induct fixp_induct_user phi =
   let
-    val term = Morphism.term phi;
-    val thm = Morphism.thm phi;
-    val data' = Setup_Data 
-      {fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq,
-       fixp_induct=thm fixp_induct, fixp_induct_user=Option.map thm fixp_induct_user};
-  in
-    Modes.map (Symtab.update (mode, data'))
-  end
+    val data' =
+      Setup_Data
+       {fixp = fixp, mono = mono, fixp_eq = fixp_eq,
+        fixp_induct = fixp_induct, fixp_induct_user = fixp_induct_user}
+      |> transform_setup_data (phi $> Morphism.trim_context_morphism);
+  in Modes.map (Symtab.update (mode, data')) end;
 
 val known_modes = Symtab.keys o Modes.get o Context.Proof;
-val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;
+
+fun lookup_mode ctxt =
+  Symtab.lookup (Modes.get (Context.Proof ctxt))
+  #> Option.map (transform_setup_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
 
 
 (*** Automated monotonicity proofs ***)
@@ -159,7 +166,7 @@
   let
     val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
     val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
-  in 
+  in
     (* FIXME ctxt vs. ctxt' (!?) *)
     rule
     |> infer_instantiate' ctxt
@@ -182,7 +189,7 @@
     val split_paired_all_conv =
       Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all}))
 
-    val split_params_conv = 
+    val split_params_conv =
       Conv.params_conv ~1 (fn ctxt' =>
         Conv.implies_conv split_paired_all_conv Conv.all_conv)
 
@@ -207,7 +214,7 @@
   in
     inst_rule'
   end;
-    
+
 
 (*** partial_function definition ***)
 
@@ -264,7 +271,7 @@
         OF [inst_mono_thm, f_def])
       |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
 
-    val specialized_fixp_induct = 
+    val specialized_fixp_induct =
       specialize_fixp_induct lthy' args fT fT_uc F curry uncurry inst_mono_thm f_def fixp_induct
       |> Drule.rename_bvars' (map SOME (fname :: fname :: argnames));
 
@@ -288,10 +295,10 @@
     |-> (fn (_, rec') =>
       Spec_Rules.add Spec_Rules.Equational ([f], rec')
       #> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec') #> snd)
-    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "mono"), []), [mono_thm]) #> snd) 
+    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "mono"), []), [mono_thm]) #> snd)
     |> (case raw_induct of NONE => I | SOME thm =>
          Local_Theory.note ((Binding.qualify true fname (Binding.name "raw_induct"), []), [thm]) #> snd)
-    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "fixp_induct"), []), [specialized_fixp_induct]) #> snd) 
+    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "fixp_induct"), []), [specialized_fixp_induct]) #> snd)
   end;
 
 val add_partial_function = gen_add_partial_function Specification.check_spec;
@@ -304,4 +311,4 @@
     ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
       >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
 
-end
+end;
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -186,7 +186,7 @@
       |> Sign.parent_path
       |> fold_map
         (fn (((name, mx), tvs), c) =>
-          Typedef.add_typedef_global false (name, tvs, mx)
+          Typedef.add_typedef_global (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (fn ctxt =>
               resolve_tac ctxt [exI] 1 THEN
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Predicate_Compile/mode_inference.ML
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -53,7 +53,7 @@
 struct
 
 open Predicate_Compile_Aux;
-open Core_Data;
+
 
 (* derivation trees for modes of premises *)
 
@@ -317,7 +317,7 @@
         fun is_functional t mode =
           case try (fst o dest_Const o fst o strip_comb) t of
             NONE => false
-          | SOME c => is_some (alternative_compilation_of ctxt c mode)
+          | SOME c => is_some (Core_Data.alternative_compilation_of ctxt c mode)
       in
         case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
           (true, true) => EQUAL
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -72,7 +72,6 @@
 type random_seed = Random_Engine.seed
 
 open Predicate_Compile_Aux;
-open Core_Data;
 open Mode_Inference;
 open Predicate_Compile_Proof;
 
@@ -126,18 +125,19 @@
 
 fun print_stored_rules ctxt =
   let
-    val preds = Graph.keys (PredData.get (Proof_Context.theory_of ctxt))
-    fun print pred () = let
-      val _ = writeln ("predicate: " ^ pred)
-      val _ = writeln ("introrules: ")
-      val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
-        (rev (intros_of ctxt pred)) ()
-    in
-      if (has_elim ctxt pred) then
-        writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred))
-      else
-        writeln ("no elimrule defined")
-    end
+    val preds = Graph.keys (Core_Data.PredData.get (Proof_Context.theory_of ctxt))
+    fun print pred () =
+      let
+        val _ = writeln ("predicate: " ^ pred)
+        val _ = writeln ("introrules: ")
+        val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
+          (rev (Core_Data.intros_of ctxt pred)) ()
+      in
+        if Core_Data.has_elim ctxt pred then
+          writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
+        else
+          writeln ("no elimrule defined")
+      end
   in
     fold print preds ()
   end;
@@ -151,7 +151,7 @@
         val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
       in u end
   in
-    fold print (all_modes_of compilation ctxt) ()
+    fold print (Core_Data.all_modes_of compilation ctxt) ()
   end
 
 (* validity checks *)
@@ -670,10 +670,10 @@
           SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
       | (_, Term Output) => NONE
       | (Const (name, T), Context mode) =>
-          (case alternative_compilation_of ctxt name mode of
+          (case Core_Data.alternative_compilation_of ctxt name mode of
             SOME alt_comp => SOME (alt_comp compfuns T)
           | NONE =>
-            SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+            SOME (Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers)
               ctxt name mode,
               Comp_Mod.funT_of compilation_modifiers mode T)))
       | (Free (s, T), Context m) =>
@@ -1014,7 +1014,7 @@
               foldr1 (mk_plus compfuns) cl_ts)
         end
     val fun_const =
-      Const (function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
+      Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
   in
     HOLogic.mk_Trueprop
       (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
@@ -1132,7 +1132,7 @@
         val mode_cname = create_constname_of_mode options thy "" name T mode
         val mode_cbasename = Long_Name.base_name mode_cname
         val funT = funT_of compfuns mode T
-        val (args, _) = fold_map (mk_args true) ((strip_fun_mode mode) ~~ (binder_types T)) []
+        val (args, _) = fold_map (mk_args true) (strip_fun_mode mode ~~ binder_types T) []
         fun strip_eval _ t =
           let
             val t' = strip_split_abs t
@@ -1152,13 +1152,13 @@
           create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
         in
           thy'
-          |> set_function_name Pred name mode mode_cname
-          |> add_predfun_data name mode (definition, rules)
+          |> Core_Data.set_function_name Pred name mode mode_cname
+          |> Core_Data.add_predfun_data name mode (definition, rules)
           |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
           |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
         end;
   in
-    thy |> defined_function_of Pred name |> fold create_definition modes
+    thy |> Core_Data.defined_function_of Pred name |> fold create_definition modes
   end;
 
 fun define_functions comp_modifiers _ options preds (name, modes) thy =
@@ -1171,11 +1171,11 @@
         val funT = Comp_Mod.funT_of comp_modifiers mode T
       in
         thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
+        |> Core_Data.set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
       end;
   in
     thy
-    |> defined_function_of (Comp_Mod.compilation comp_modifiers) name
+    |> Core_Data.defined_function_of (Comp_Mod.compilation comp_modifiers) name
     |> fold create_definition modes
   end;
 
@@ -1220,7 +1220,7 @@
           Syntax.string_of_term ctxt (c $ t))
       | Sidecond t => Sidecond (c $ t))
   | (Const (s, _), _) =>
-      if is_registered ctxt s then Prem t else Sidecond t
+      if Core_Data.is_registered ctxt s then Prem t else Sidecond t
   | _ => Sidecond t)
 
 fun prepare_intrs options ctxt prednames intros =
@@ -1334,18 +1334,18 @@
       let
         val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
       in
-        if member eq_mode  (modes_of Pred ctxt predname) full_mode then
+        if member eq_mode (Core_Data.modes_of Pred ctxt predname) full_mode then
           let
             val Ts = binder_types T
             val arg_names = Name.variant_list []
               (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
             val args = map2 (curry Free) arg_names Ts
-            val predfun = Const (function_name_of Pred ctxt predname full_mode,
+            val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode,
               Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit})
             val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
-            val def = predfun_definition_of ctxt predname full_mode
+            val def = Core_Data.predfun_definition_of ctxt predname full_mode
             val tac = fn _ => Simplifier.simp_tac
               (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
             val eq = Goal.prove ctxt arg_names [] eq_term tac
@@ -1387,18 +1387,18 @@
     (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
     val _ =
       if show_intermediate_results options then
-        tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
+        tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
       else ()
     val (preds, all_vs, param_vs, all_modes, clauses) =
-      prepare_intrs options ctxt prednames (maps (intros_of ctxt) prednames)
+      prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames)
     val _ = print_step options "Infering modes..."
-    val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
-      modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
+    val (lookup_mode, lookup_neg_mode, needs_random) = (Core_Data.modes_of compilation ctxt,
+      Core_Data.modes_of (negative_compilation_of compilation) ctxt, Core_Data.needs_random ctxt)
     val ((moded_clauses, needs_random), errors) =
       cond_timeit (Config.get ctxt Quickcheck.timing) "Infering modes"
       (fn _ => infer_modes mode_analysis_options
         options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
-    val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
+    val thy' = fold (fn (s, ms) => Core_Data.set_needs_random s ms) needs_random thy
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes options preds modes
     val _ = check_proposed_modes options preds modes errors
@@ -1435,12 +1435,12 @@
 fun gen_add_equations steps options names thy =
   let
     fun dest_steps (Steps s) = s
-    val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
-    val thy' = extend_intro_graph names thy;
+    val defined = Core_Data.defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
+    val thy' = Core_Data.extend_intro_graph names thy;
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
-    val scc = strong_conn_of (PredData.get thy') names
-    val thy'' = fold preprocess_intros (flat scc) thy'
+    val scc = strong_conn_of (Core_Data.PredData.get thy') names
+    val thy'' = fold Core_Data.preprocess_intros (flat scc) thy'
     val thy''' = fold_rev
       (fn preds => fn thy =>
         if not (forall (defined (Proof_Context.init_global thy)) preds) then
@@ -1601,7 +1601,7 @@
 fun attrib' f opt_case_name =
   Thm.declaration_attribute (fn thm => Context.mapping (f (opt_case_name, thm)) I);
 
-val code_pred_intro_attrib = attrib' add_intro NONE;
+val code_pred_intro_attrib = attrib' Core_Data.add_intro NONE;
 
 (*FIXME
 - Naming of auxiliary rules necessary?
@@ -1616,8 +1616,9 @@
 
 val _ =
   Theory.setup
-   (PredData.put (Graph.empty) #>
-    Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
+   (Core_Data.PredData.put (Graph.empty) #>
+    Attrib.setup @{binding code_pred_intro}
+      (Scan.lift (Scan.option Args.name) >> attrib' Core_Data.add_intro)
       "adding alternative introduction rules for code generation of inductive predicates")
 
 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
@@ -1626,15 +1627,16 @@
   let
     val thy = Proof_Context.theory_of lthy
     val const = prep_const thy raw_const
-    val lthy' = Local_Theory.background_theory (extend_intro_graph [const]) lthy
+    val lthy' = Local_Theory.background_theory (Core_Data.extend_intro_graph [const]) lthy
     val thy' = Proof_Context.theory_of lthy'
     val ctxt' = Proof_Context.init_global thy'
-    val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
+    val preds =
+      Graph.all_succs (Core_Data.PredData.get thy') [const] |> filter_out (Core_Data.has_elim ctxt')
     fun mk_cases const =
       let
         val T = Sign.the_const_type thy' const
         val pred = Const (const, T)
-        val intros = intros_of ctxt' const
+        val intros = Core_Data.intros_of ctxt' const
       in mk_casesrule lthy' pred intros end
     val cases_rules = map mk_cases preds
     val cases =
@@ -1644,7 +1646,7 @@
           assumes =
             ("that", tl (Logic.strip_imp_prems case_rule)) ::
             map_filter (fn (fact_name, fact) => Option.map (fn a => (a, [fact])) fact_name)
-              ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
+              ((SOME "prems" :: Core_Data.names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
           binds = [], cases = []}) preds cases_rules
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     val lthy'' = lthy'
@@ -1655,7 +1657,7 @@
         val global_thms = Proof_Context.export goal_ctxt
           (Proof_Context.init_global (Proof_Context.theory_of goal_ctxt)) (map the_single thms)
       in
-        goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #>
+        goal_ctxt |> Local_Theory.background_theory (fold Core_Data.set_elim global_thms #>
           ((case compilation options of
              Pred => add_equations
            | DSeq => add_dseq_equations
@@ -1762,7 +1764,7 @@
   (compilation, _) t_compr =
   let
     val compfuns = Comp_Mod.compfuns comp_modifiers
-    val all_modes_of = all_modes_of compilation
+    val all_modes_of = Core_Data.all_modes_of compilation
     val (((body, output), T_compr), output_names) =
       (case try dest_special_compr t_compr of
         SOME r => r
@@ -1772,7 +1774,7 @@
         (Const (name, T), all_args) => (Const (name, T), all_args)
       | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head))
   in
-    if defined_functions compilation ctxt name then
+    if Core_Data.defined_functions compilation ctxt name then
       let
         fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) =
               Pair (extract_mode t1, extract_mode t2)
@@ -1878,7 +1880,6 @@
             @{term natural_of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
       else
         mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
-    val thy = Proof_Context.theory_of ctxt
     val time_limit = seconds (Config.get ctxt values_timeout)
     val (ts, statistics) =
       (case compilation of
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -12,14 +12,13 @@
     -> (string * (term list * indprem list) list) list
     -> (string * typ) list -> string -> bool * mode
     -> (term list * (indprem * Mode_Inference.mode_derivation) list) list * term
-    -> Thm.thm
+    -> thm
 end;
 
 structure Predicate_Compile_Proof : PREDICATE_COMPILE_PROOF =
 struct
 
 open Predicate_Compile_Aux;
-open Core_Data;
 open Mode_Inference;
 
 
@@ -62,7 +61,7 @@
     val f_tac =
       (case f of
         Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-           [@{thm eval_pred}, predfun_definition_of ctxt name mode,
+           [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
            @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
            @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
       | Free _ =>
@@ -88,7 +87,7 @@
     (Const (name, _), args) =>
       let
         val mode = head_mode_of deriv
-        val introrule = predfun_intro_of ctxt name mode
+        val introrule = Core_Data.predfun_intro_of ctxt name mode
         val param_derivations = param_derivations_of deriv
         val ho_args = ho_args_of mode args
       in
@@ -170,12 +169,12 @@
     fun preds_of t nameTs =
       (case strip_comb t of
         (Const (name, T), args) =>
-          if is_registered ctxt name then (name, T) :: nameTs
-            else fold preds_of args nameTs
+          if Core_Data.is_registered ctxt name then (name, T) :: nameTs
+          else fold preds_of args nameTs
       | _ => nameTs)
     val preds = preds_of t []
     val defs = map
-      (fn (pred, T) => predfun_definition_of ctxt pred
+      (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred
         (all_input_of T))
         preds
   in
@@ -227,7 +226,7 @@
                 val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
                 val neg_intro_rule =
                   Option.map (fn name =>
-                    the (predfun_neg_intro_of ctxt name mode)) name
+                    the (Core_Data.predfun_neg_intro_of ctxt name mode)) name
                 val param_derivations = param_derivations_of deriv
                 val params = ho_args_of mode args
               in
@@ -278,11 +277,11 @@
   let
     val T = the (AList.lookup (op =) preds pred)
     val nargs = length (binder_types T)
-    val pred_case_rule = the_elim_of ctxt pred
+    val pred_case_rule = Core_Data.the_elim_of ctxt pred
   in
     REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
     THEN trace_tac ctxt options "before applying elim rule"
-    THEN eresolve_tac ctxt [predfun_elim_of ctxt pred mode] 1
+    THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt pred mode] 1
     THEN eresolve_tac ctxt [pred_case_rule] 1
     THEN trace_tac ctxt options "after applying elim rule"
     THEN (EVERY (map
@@ -338,8 +337,8 @@
     val f_tac =
       (case f of
         Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-           (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
-           :: @{thm "Product_Type.split_conv"}::[])) 1
+           [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
+            @{thm Product_Type.split_conv}]) 1
       | Free _ => all_tac
       | _ => error "prove_param2: illegal parameter term")
   in
@@ -360,7 +359,7 @@
           eresolve_tac ctxt @{thms bindE} 1
           THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
           THEN trace_tac ctxt options "prove_expr2-before"
-          THEN eresolve_tac ctxt [predfun_elim_of ctxt name mode] 1
+          THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt name mode] 1
           THEN trace_tac ctxt options "prove_expr2"
           THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
           THEN trace_tac ctxt options "finished prove_expr2"
@@ -372,12 +371,12 @@
     fun preds_of t nameTs =
       (case strip_comb t of
         (Const (name, T), args) =>
-          if is_registered ctxt name then (name, T) :: nameTs
-            else fold preds_of args nameTs
+          if Core_Data.is_registered ctxt name then (name, T) :: nameTs
+          else fold preds_of args nameTs
       | _ => nameTs)
     val preds = preds_of t []
     val defs = map
-      (fn (pred, T) => predfun_definition_of ctxt pred
+      (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred
         (all_input_of T))
         preds
   in
@@ -389,7 +388,7 @@
 
 fun prove_clause2 options ctxt pred mode (ts, ps) i =
   let
-    val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
+    val pred_intro_rule = nth (Core_Data.intros_of ctxt pred) (i - 1)
     val (in_ts, _) = split_mode mode ts;
     val split_simpset =
       put_simpset HOL_basic_ss' ctxt
@@ -441,9 +440,9 @@
                 THEN eresolve_tac ctxt @{thms bindE} 1
                 THEN (if is_some name then
                     full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-                      [predfun_definition_of ctxt (the name) mode]) 1
+                      [Core_Data.predfun_definition_of ctxt (the name) mode]) 1
                     THEN eresolve_tac ctxt @{thms not_predE} 1
-                    THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
+                    THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms not_False_eq_True}) 1
                     THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
                   else
                     eresolve_tac ctxt @{thms not_predE'} 1)
@@ -478,7 +477,7 @@
   in
     (DETERM (TRY (resolve_tac ctxt @{thms unit.induct} 1)))
      THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
-     THEN (resolve_tac ctxt [predfun_intro_of ctxt pred mode] 1)
+     THEN (resolve_tac ctxt [Core_Data.predfun_intro_of ctxt pred mode] 1)
      THEN (REPEAT_DETERM (resolve_tac ctxt @{thms refl} 2))
      THEN (
        if null moded_clauses then eresolve_tac ctxt @{thms botE} 1
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -45,7 +45,7 @@
     fun typedef_tac ctxt =
       EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
   in
-    Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx)
+    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
       (typedef_term rel rty lthy) NONE typedef_tac lthy
   end
 
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/record.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -99,7 +99,7 @@
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
-    |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
+    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
         (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
diff -r 279a5b4f47bd -r 4b5872b9d783 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -16,16 +16,20 @@
   val get_info: Proof.context -> string -> info list
   val get_info_global: theory -> string -> info list
   val interpretation: (string -> local_theory -> local_theory) -> theory -> theory
-  val add_typedef: bool -> binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> (Proof.context -> tactic) -> local_theory ->
+  type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding}
+  val default_bindings: binding -> bindings
+  val make_bindings: binding -> bindings option -> bindings
+  val make_morphisms: binding -> (binding * binding) option -> bindings
+  val add_typedef: binding * (string * sort) list * mixfix ->
+    term -> bindings option -> (Proof.context -> tactic) -> local_theory ->
     (string * info) * local_theory
-  val add_typedef_global: bool -> binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> (Proof.context -> tactic) -> theory ->
+  val add_typedef_global: binding * (string * sort) list * mixfix ->
+    term -> bindings option -> (Proof.context -> tactic) -> theory ->
     (string * info) * theory
-  val typedef: (binding * (string * sort) list * mixfix) * term *
-    (binding * binding) option -> local_theory -> Proof.state
-  val typedef_cmd: (binding * (string * string option) list * mixfix) * string *
-    (binding * binding) option -> local_theory -> Proof.state
+  val typedef: binding * (string * sort) list * mixfix -> term -> bindings option ->
+    local_theory -> Proof.state
+  val typedef_cmd: binding * (string * string option) list * mixfix -> string -> bindings option ->
+    local_theory -> Proof.state
 end;
 
 structure Typedef: TYPEDEF =
@@ -105,7 +109,7 @@
         (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
   in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
 
-fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A lthy =
+fun primitive_typedef type_definition_name newT oldT Rep_name Abs_name A lthy =
   let
     (* errors *)
 
@@ -133,18 +137,35 @@
 
     val ((axiom_name, axiom), axiom_lthy) = consts_lthy
       |> Local_Theory.background_theory_result
-        (Thm.add_axiom consts_lthy (typedef_name, mk_typedef newT oldT RepC AbsC A) ##>
+        (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##>
           Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##>
           Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps);
 
   in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
 
 
+(* derived bindings *)
+
+type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding};
+
+fun default_bindings name =
+ {Rep_name = Binding.prefix_name "Rep_" name,
+  Abs_name = Binding.prefix_name "Abs_" name,
+  type_definition_name = Binding.prefix_name "type_definition_" name};
+
+fun make_bindings name NONE = default_bindings name
+  | make_bindings _ (SOME bindings) = bindings;
+
+fun make_morphisms name NONE = default_bindings name
+  | make_morphisms name (SOME (Rep_name, Abs_name)) =
+      {Rep_name = Rep_name, Abs_name = Abs_name,
+        type_definition_name = #type_definition_name (default_bindings name)};
+
+
 (* prepare_typedef *)
 
-fun prepare_typedef concealed prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
+fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_bindings lthy =
   let
-    val concealed_name = name |> concealed ? Binding.concealed;
     val bname = Binding.name_of name;
 
 
@@ -174,16 +195,10 @@
 
     (* axiomatization *)
 
-    val (Rep_name, Abs_name) =
-      (case opt_morphs of
-        NONE => (Binding.prefix_name "Rep_" concealed_name,
-          Binding.prefix_name "Abs_" concealed_name)
-      | SOME morphs => morphs);
-
-    val typedef_name = Binding.prefix_name "type_definition_" concealed_name;
+    val {Rep_name, Abs_name, type_definition_name} = make_bindings name opt_bindings;
 
     val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
-      |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set;
+      |> primitive_typedef type_definition_name newT oldT Rep_name Abs_name set;
 
     val alias_lthy = typedef_lthy
       |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
@@ -202,7 +217,7 @@
         fun make th = Goal.norm_result lthy1 (typedef' RS th);
         val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
             Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
-          |> Local_Theory.note ((typedef_name, []), [typedef'])
+          |> Local_Theory.note ((type_definition_name, []), [typedef'])
           ||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep})
           ||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []),
               make @{thm type_definition.Rep_inverse})
@@ -247,18 +262,18 @@
 
 (* add_typedef: tactic interface *)
 
-fun add_typedef concealed typ set opt_morphs tac lthy =
+fun add_typedef typ set opt_bindings tac lthy =
   let
     val ((goal, _, typedef_result), lthy') =
-      prepare_typedef concealed Syntax.check_term typ set opt_morphs lthy;
+      prepare_typedef Syntax.check_term typ set opt_bindings lthy;
     val inhabited =
       Goal.prove lthy' [] [] goal (tac o #context)
       |> Goal.norm_result lthy' |> Thm.close_derivation;
   in typedef_result inhabited lthy' end;
 
-fun add_typedef_global concealed typ set opt_morphs tac =
+fun add_typedef_global typ set opt_bindings tac =
   Named_Target.theory_init
-  #> add_typedef concealed typ set opt_morphs tac
+  #> add_typedef typ set opt_bindings tac
   #> Local_Theory.exit_result_global (apsnd o transform_info);
 
 
@@ -266,11 +281,11 @@
 
 local
 
-fun gen_typedef prep_term prep_constraint ((b, raw_args, mx), set, opt_morphs) lthy =
+fun gen_typedef prep_term prep_constraint (b, raw_args, mx) set opt_bindings lthy =
   let
     val args = map (apsnd (prep_constraint lthy)) raw_args;
     val ((goal, goal_pat, typedef_result), lthy') =
-      prepare_typedef false prep_term (b, args, mx) set opt_morphs lthy;
+      prepare_typedef prep_term (b, args, mx) set opt_bindings lthy;
     fun after_qed [[th]] = snd o typedef_result th;
   in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
 
@@ -291,6 +306,7 @@
     (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
       (@{keyword "="} |-- Parse.term) --
       Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-    >> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));
+    >> (fn ((((vs, t), mx), A), opt_morphs) => fn lthy =>
+        typedef_cmd (t, vs, mx) A (SOME (make_morphisms t opt_morphs)) lthy));
 
 end;
diff -r 279a5b4f47bd -r 4b5872b9d783 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -368,10 +368,11 @@
 fun init_target background_naming operations after_close lthy =
   let
     val _ = assert lthy;
+    val after_close' = Proof_Context.restore_naming lthy #> after_close;
     val (scope, target) = Proof_Context.new_scope lthy;
     val lthy' =
       target
-      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target)));
   in (scope, lthy') end;
 
 fun open_target lthy =
diff -r 279a5b4f47bd -r 4b5872b9d783 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Sep 04 09:15:15 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Sep 04 22:16:54 2015 +0200
@@ -1083,8 +1083,9 @@
     val goal_ctxt = ctxt
       |> (fold o fold) Variable.auto_fixes propss
       |> fold Variable.bind_term binds;
-    fun after_qed' (result_ctxt, results) ctxt' =
-      after_qed (burrow (Proof_Context.export result_ctxt ctxt') results) ctxt';
+    fun after_qed' (result_ctxt, results) ctxt' = ctxt'
+      |> Proof_Context.restore_naming ctxt
+      |> after_qed (burrow (Proof_Context.export result_ctxt ctxt') results);
   in
     ctxt
     |> init