# HG changeset patch
# User wenzelm
# Date 1443094422 -7200
# Node ID e6f03fae14d59862a4687ea67d9383a0f4a08d00
# Parent  6dc3d5d50e57c89ee3b7d0b9f364fc3e3c51c5fd
explicit indication of overloaded typedefs;

diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -932,7 +932,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
+    @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \<newline>
       (@{syntax type} '+')? (constdecl +)
     ;
     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
@@ -1131,7 +1131,9 @@
   definition, but less powerful in practice.
 
   @{rail \<open>
-    @@{command (HOL) typedef} abs_type '=' rep_set
+    @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
+    ;
+    @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
     ;
     abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
     ;
@@ -1185,6 +1187,13 @@
   for the generic @{method cases} and @{method induct} methods,
   respectively.
 
+  \medskip The ``@{text "(overloaded)"}'' option allows the @{command
+  "typedef"} specification to depend on constants that are not (yet)
+  specified and thus left open as parameters. In particular, a @{command
+  typedef} depending on type-class parameters (cf.\ \secref{sec:class}) is
+  semantically like a dependent type: its meaning is determined for
+  different type-class instances according to their respective operations.
+
   \end{description}
 \<close>
 
@@ -1299,8 +1308,9 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '='
-      quot_type \<newline> quot_morphisms? quot_parametric?
+    @@{command (HOL) quotient_type} @{syntax "overloaded"}? \<newline>
+      @{syntax typespec} @{syntax mixfix}? '=' quot_type \<newline>
+      quot_morphisms? quot_parametric?
     ;
     quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
     ;
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Datatype_Examples/Misc_N2M.thy
--- a/src/HOL/Datatype_Examples/Misc_N2M.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Datatype_Examples/Misc_N2M.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -11,6 +11,9 @@
 imports "~~/src/HOL/Library/BNF_Axiomatization"
 begin
 
+declare [[typedef_overloaded]]
+
+
 locale misc
 begin
 
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Datatype_Examples/Stream_Processor.thy
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -12,6 +12,9 @@
 imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
 begin
 
+declare [[typedef_overloaded]]
+
+
 section {* Continuous Functions on Streams *}
 
 datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/HOLCF/Porder.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -8,6 +8,9 @@
 imports Main
 begin
 
+declare [[typedef_overloaded]]
+
+
 subsection {* Type class for partial orders *}
 
 class below =
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -165,7 +165,7 @@
   let
     val name = #1 typ
     val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
-      |> Typedef.add_typedef_global typ set opt_bindings tac
+      |> Typedef.add_typedef_global {overloaded = false} 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))
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -19,7 +19,7 @@
 
 hide_type st  --"hide previous def to avoid long names"
 
-quotient_type 'a st = "('a::top) st_rep" / eq_st
+quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st
 morphisms rep_st St
 by (metis eq_st_def equivpI reflpI sympI transpI)
 
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Import/import_rule.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -222,7 +222,8 @@
       Typedef.make_morphisms (Binding.name tycname)
         (SOME (Binding.name rep_name, Binding.name abs_name))
     val ((_, typedef_info), thy') =
-     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
+     Typedef.add_typedef_global {overloaded = false}
+       (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))
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -47,7 +47,7 @@
 
 end
 
-quotient_type 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
+quotient_type (overloaded) 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
 by(rule part_equivp_fractrel)
 
 subsubsection \<open>Representation and basic operations\<close>
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -52,7 +52,7 @@
 
 subsection \<open>Definition of type @{text poly}\<close>
 
-typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
+typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
   morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
 
 setup_lifting type_definition_poly
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Library/Quotient_Type.thy
--- a/src/HOL/Library/Quotient_Type.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Quotient_Type.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -62,7 +62,7 @@
 
 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
 
-typedef 'a quot = "quot :: 'a::eqv set set"
+typedef (overloaded) 'a quot = "quot :: 'a::eqv set set"
   unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/RBT.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -10,7 +10,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
   morphisms impl_of RBT
 proof -
   have "RBT_Impl.Empty \<in> ?rbt" by simp
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Saturated.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -12,7 +12,7 @@
 
 subsection \<open>The type of saturated naturals\<close>
 
-typedef ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}"
   morphisms nat_of Abs_sat
   by auto
 
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -13,7 +13,7 @@
 
 definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
 
-typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
+typedef (overloaded) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
   unfolding matrix_def
 proof
   show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -9,7 +9,8 @@
 definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
   where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
 
-typedef ('a, 'b) bcontfun = "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
+typedef (overloaded) ('a, 'b) bcontfun =
+    "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
   by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
 
 lemma bcontfunE:
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -6,6 +6,9 @@
   "avoids"
 begin
 
+declare [[typedef_overloaded]]
+
+
 section {* Permutations *}
 (*======================*)
 
@@ -3378,7 +3381,7 @@
 
 definition "ABS = ABS_set"
 
-typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
     "ABS::('x\<Rightarrow>('a noption)) set"
   morphisms Rep_ABS Abs_ABS
   unfolding ABS_def
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -586,7 +586,7 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
-          Typedef.add_typedef_global
+          Typedef.add_typedef_global {overloaded = false}
             (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 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -359,7 +359,7 @@
          map (rpair (mk_type thy prfx ty)) flds) fldtys
        in case get_type thy prfx s of
            NONE =>
-             Record.add_record ([], Binding.name s) NONE
+             Record.add_record {overloaded = false} ([], Binding.name s) NONE
                (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
          | SOME (rT, cmap) =>
              (case get_record_info thy rT of
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -156,7 +156,7 @@
     val ((name, info), (lthy, lthy_old)) =
       lthy
       |> Local_Theory.open_target |> snd
-      |> Typedef.add_typedef (b', Ts, mx) set (SOME bindings) tac
+      |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac
       ||> `Local_Theory.close_target;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -186,7 +186,7 @@
       |> Sign.parent_path
       |> fold_map
         (fn (((name, mx), tvs), c) =>
-          Typedef.add_typedef_global (name, tvs, mx)
+          Typedef.add_typedef_global {overloaded = false} (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (fn ctxt =>
               resolve_tac ctxt [exI] 1 THEN
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -6,14 +6,17 @@
 
 signature QUOTIENT_TYPE =
 sig
-  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
-    ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
-
-  val quotient_type: (string list * binding * mixfix) * (typ * term * bool) *
-    ((binding * binding) option * thm option) -> Proof.context -> Proof.state
-
-  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
-    (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
+  val add_quotient_type: {overloaded: bool} ->
+    ((string list * binding * mixfix) * (typ * term * bool) *
+      ((binding * binding) option * thm option)) * thm -> local_theory ->
+      Quotient_Info.quotients * local_theory
+  val quotient_type:  {overloaded: bool} ->
+    (string list * binding * mixfix) * (typ * term * bool) *
+      ((binding * binding) option * thm option) -> Proof.context -> Proof.state
+  val quotient_type_cmd:  {overloaded: bool} ->
+    (((((string list * binding) * mixfix) * string) * (bool * string)) *
+      (binding * binding) option) * (Facts.ref * Token.src list) option ->
+      Proof.context -> Proof.state
 end;
 
 structure Quotient_Type: QUOTIENT_TYPE =
@@ -40,12 +43,12 @@
 
 
 (* makes the new type definitions and proves non-emptyness *)
-fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
+fun typedef_make overloaded (vs, qty_name, mx, rel, rty) equiv_thm lthy =
   let
     fun typedef_tac ctxt =
       EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
   in
-    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
+    Typedef.add_typedef overloaded (qty_name, map (rpair dummyS) vs, mx)
       (typedef_term rel rty lthy) NONE typedef_tac lthy
   end
 
@@ -152,7 +155,8 @@
   end
 
 (* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
+fun add_quotient_type overloaded
+    (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
   let
     val part_equiv =
       if partial
@@ -161,7 +165,7 @@
 
     (* generates the typedef *)
     val ((_, typedef_info), lthy1) =
-      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
+      typedef_make overloaded (vs, qty_name, mx, rel, rty) part_equiv lthy
 
     (* abs and rep functions from the typedef *)
     val Abs_ty = #abs_type (#1 typedef_info)
@@ -290,7 +294,7 @@
  relations are equivalence relations
 *)
 
-fun quotient_type quot lthy =
+fun quotient_type overloaded quot lthy =
   let
     (* sanity check *)
     val _ = sanity_check quot
@@ -307,12 +311,12 @@
 
     val goal = (mk_goal o #2) quot
 
-    fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm)
+    fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm)
   in
     Proof.theorem NONE after_qed [[(goal, [])]] lthy
   end
 
-fun quotient_type_cmd spec lthy =
+fun quotient_type_cmd overloaded spec lthy =
   let
     fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
       let
@@ -330,7 +334,7 @@
 
     val (spec', _) = parse_spec spec lthy
   in
-    quotient_type spec' lthy
+    quotient_type overloaded spec' lthy
   end
 
 
@@ -340,11 +344,11 @@
   Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
     "quotient type definitions (require equivalence proofs)"
       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
-      (Parse.type_args -- Parse.binding --
+      (Parse_Spec.overloaded -- (Parse.type_args -- Parse.binding --
         Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
           Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
-        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
-      >> quotient_type_cmd)
+        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
+      >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
 
 end
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/record.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -26,8 +26,8 @@
   val get_info: theory -> string -> info option
   val the_info: theory -> string -> info
   val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
-  val add_record: (string * sort) list * binding -> (typ list * string) option ->
-    (binding * typ * mixfix) list -> theory -> theory
+  val add_record: {overloaded: bool} -> (string * sort) list * binding ->
+    (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory
 
   val last_extT: typ -> (string * typ list) option
   val dest_recTs: typ -> (string * typ list) list
@@ -55,7 +55,7 @@
 
 signature ISO_TUPLE_SUPPORT =
 sig
-  val add_iso_tuple_type: binding * (string * sort) list ->
+  val add_iso_tuple_type: {overloaded: bool} -> binding * (string * sort) list ->
     typ * typ -> theory -> (term * term) * theory
   val mk_cons_tuple: term * term -> term
   val dest_cons_tuple: term -> term * term
@@ -93,13 +93,13 @@
     |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
   end
 
-fun do_typedef raw_tyco repT raw_vs thy =
+fun do_typedef overloaded raw_tyco repT raw_vs thy =
   let
     val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
-    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
+    |> Typedef.add_typedef_global overloaded (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;
@@ -117,13 +117,13 @@
 fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
   | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
 
-fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
+fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy =
   let
     val repT = HOLogic.mk_prodT (leftT, rightT);
 
     val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
       thy
-      |> do_typedef b repT alphas
+      |> do_typedef overloaded b repT alphas
       ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
     val typ_ctxt = Proof_Context.init_global typ_thy;
 
@@ -1499,7 +1499,7 @@
   in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end);
 
 
-fun extension_definition name fields alphas zeta moreT more vars thy =
+fun extension_definition overloaded name fields alphas zeta moreT more vars thy =
   let
     val ctxt = Proof_Context.init_global thy;
 
@@ -1525,7 +1525,7 @@
       let
         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
         val ((_, cons), thy') = thy
-          |> Iso_Tuple_Support.add_iso_tuple_type
+          |> Iso_Tuple_Support.add_iso_tuple_type overloaded
             (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
               (fastype_of left, fastype_of right);
       in
@@ -1808,7 +1808,7 @@
 
 (* definition *)
 
-fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
+fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
   let
     val ctxt0 = Proof_Context.init_global thy0;
 
@@ -1867,7 +1867,7 @@
         extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
       thy0
       |> Sign.qualified_path false binding
-      |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
+      |> extension_definition overloaded extension_name fields alphas_ext zeta moreT more vars;
     val ext_ctxt = Proof_Context.init_global ext_thy;
 
     val _ = timing_msg ext_ctxt "record preparing definitions";
@@ -2277,7 +2277,7 @@
 
 in
 
-fun add_record (params, binding) raw_parent raw_fields thy =
+fun add_record overloaded (params, binding) raw_parent raw_fields thy =
   let
     val ctxt = Proof_Context.init_global thy;
     fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
@@ -2327,11 +2327,11 @@
       err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
     val _ = if null errs then () else error (cat_lines errs);
   in
-    thy |> definition (params, binding) parent parents bfields
+    thy |> definition overloaded (params, binding) parent parents bfields
   end
   handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
 
-fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
+fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fields thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
@@ -2339,7 +2339,7 @@
     val (parent, ctxt2) = read_parent raw_parent ctxt1;
     val (fields, ctxt3) = read_fields raw_fields ctxt2;
     val params' = map (Proof_Context.check_tfree ctxt3) params;
-  in thy |> add_record (params', binding) parent fields end;
+  in thy |> add_record overloaded (params', binding) parent fields end;
 
 end;
 
@@ -2348,9 +2348,10 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword record} "define extensible record"
-    (Parse.type_args_constrained -- Parse.binding --
+    (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) --
       (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
         Scan.repeat1 Parse.const_binding)
-    >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
+    >> (fn ((overloaded, x), (y, z)) =>
+        Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
 
 end;
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -20,16 +20,17 @@
   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 ->
+  val overloaded: bool Config.T
+  val add_typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
     term -> bindings option -> (Proof.context -> tactic) -> local_theory ->
     (string * info) * local_theory
-  val add_typedef_global: binding * (string * sort) list * mixfix ->
+  val add_typedef_global: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
     term -> bindings option -> (Proof.context -> tactic) -> theory ->
     (string * info) * theory
-  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
+  val typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
+    term -> bindings option -> local_theory -> Proof.state
+  val typedef_cmd: {overloaded: bool} -> binding * (string * string option) list * mixfix ->
+    string -> bindings option -> local_theory -> Proof.state
 end;
 
 structure Typedef: TYPEDEF =
@@ -98,6 +99,8 @@
 
 (* primitive typedef axiomatization -- for fresh typedecl *)
 
+val typedef_overloaded = Attrib.setup_config_bool @{binding typedef_overloaded} (K false);
+
 fun mk_inhabited A =
   let val T = HOLogic.dest_setT (Term.fastype_of A)
   in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
@@ -109,7 +112,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 type_definition_name newT oldT Rep_name Abs_name A lthy =
+fun primitive_typedef {overloaded} type_definition_name newT oldT Rep_name Abs_name A lthy =
   let
     (* errors *)
 
@@ -118,11 +121,13 @@
     val lhs_tfrees = Term.add_tfreesT newT [];
     val rhs_tfrees = Term.add_tfreesT oldT [];
     val _ =
-      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => ()
+      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of
+        [] => ()
       | extras => error ("Extra type variables in representing set: " ^ show_names extras));
 
     val _ =
-      (case Term.add_frees A [] of [] => []
+      (case Term.add_frees A [] of [] =>
+        []
       | xs => error ("Illegal variables in representing set: " ^ show_names xs));
 
 
@@ -148,6 +153,20 @@
           Theory.add_deps consts_lthy "" (const_dep (dest_Const RepC)) [newT_dep] ##>
           Theory.add_deps consts_lthy "" (const_dep (dest_Const AbsC)) [newT_dep]);
 
+    val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy);
+    val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep));
+    val _ =
+      if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then ()
+      else
+        error (Pretty.string_of (Pretty.chunks
+          [Pretty.paragraph
+            (Pretty.text "Type definition with open dependencies, use" @
+             [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1,
+              Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @
+             Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."),
+           Pretty.block [Pretty.str "  Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT],
+           Pretty.block (Pretty.str "  Deps:" :: Pretty.brk 2 ::
+             Pretty.commas (map (Defs.pretty_entry axiom_lthy) newT_deps))]))
   in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
 
 
@@ -171,7 +190,7 @@
 
 (* prepare_typedef *)
 
-fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_bindings lthy =
+fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy =
   let
     val bname = Binding.name_of name;
 
@@ -205,7 +224,7 @@
     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 type_definition_name newT oldT Rep_name Abs_name set;
+      |> primitive_typedef overloaded 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))
@@ -269,18 +288,18 @@
 
 (* add_typedef: tactic interface *)
 
-fun add_typedef typ set opt_bindings tac lthy =
+fun add_typedef overloaded typ set opt_bindings tac lthy =
   let
     val ((goal, _, typedef_result), lthy') =
-      prepare_typedef Syntax.check_term typ set opt_bindings lthy;
+      prepare_typedef Syntax.check_term overloaded 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 typ set opt_bindings tac =
+fun add_typedef_global overloaded typ set opt_bindings tac =
   Named_Target.theory_init
-  #> add_typedef typ set opt_bindings tac
+  #> add_typedef overloaded typ set opt_bindings tac
   #> Local_Theory.exit_result_global (apsnd o transform_info);
 
 
@@ -288,11 +307,11 @@
 
 local
 
-fun gen_typedef prep_term prep_constraint (b, raw_args, mx) set opt_bindings lthy =
+fun gen_typedef prep_term prep_constraint overloaded (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 prep_term (b, args, mx) set opt_bindings lthy;
+      prepare_typedef prep_term overloaded (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;
 
@@ -310,10 +329,14 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
     "HOL type definition (requires non-emptiness proof)"
-    (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
+    (Parse_Spec.overloaded -- 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), opt_morphs) => fn lthy =>
-        typedef_cmd (t, vs, mx) A (SOME (make_morphisms t opt_morphs)) lthy));
+    >> (fn (((((overloaded, vs), t), mx), A), opt_morphs) => fn lthy =>
+        typedef_cmd {overloaded = overloaded} (t, vs, mx) A
+          (SOME (make_morphisms t opt_morphs)) lthy));
+
+
+val overloaded = typedef_overloaded;
 
 end;
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Word/Word.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -18,7 +18,7 @@
 
 subsection {* Type definition *}
 
-typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
+typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
   morphisms uint Abs_word by auto
 
 lemma uint_nonnegative:
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/ex/PER.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -154,7 +154,7 @@
 
 definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
 
-typedef 'a quot = "quot :: 'a::partial_equiv set set"
+typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set"
   unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -29,6 +29,7 @@
   val obtains: Element.obtains parser
   val general_statement: (Element.context list * Element.statement) parser
   val statement_keyword: string parser
+  val overloaded: bool parser
 end;
 
 structure Parse_Spec: PARSE_SPEC =
@@ -155,4 +156,10 @@
 
 val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
 
+
+(* options *)
+
+val overloaded =
+  Scan.optional (Parse.$$$ "(" -- Parse.$$$ "overloaded" -- Parse.$$$ ")" >> K true) false;
+
 end;
diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Pure/defs.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -12,6 +12,7 @@
   val item_ord: item * item -> order
   type entry = item * typ list
   val pretty_args: Proof.context -> typ list -> Pretty.T list
+  val pretty_entry: Proof.context -> entry -> Pretty.T
   val plain_args: typ list -> bool
   type T
   type spec =
@@ -28,6 +29,7 @@
   val empty: T
   val merge: Proof.context -> T * T -> T
   val define: Proof.context -> bool -> string option -> string -> entry -> entry list -> T -> T
+  val get_deps: T -> item -> (typ list * entry list) list
 end;
 
 structure Defs: DEFS =
@@ -241,4 +243,6 @@
     val defs' = defs |> update_specs c spec;
   in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
 
+fun get_deps (Defs defs) c = reducts_of defs c;
+
 end;