# HG changeset patch
# User wenzelm
# Date 1442931469 -7200
# Node ID 066792098895000c334f33a891de777b4e7c51c5
# Parent  76148d288b2ec585667fdf4a5843588d1ab49537
tuned signature;

diff -r 76148d288b2e -r 066792098895 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Sep 22 15:58:19 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Tue Sep 22 16:17:49 2015 +0200
@@ -133,11 +133,9 @@
         (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
           Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
 
-    fun fold_type_constr f (Type (name, Ts)) = f (name,Ts) #> fold (fold_type_constr f) Ts
-      | fold_type_constr _ _ = I;
-
-    val A_consts = fold_aterms (fn Const const => insert (op =) (Theory.DConst const) | _ => I) A [];
-    val A_types = fold_types (fold_type_constr (insert (op =) o Theory.DType)) A [];
+    val A_consts = fold_aterms (fn Const c => insert (op =) (Theory.DConst c) | _ => I) A [];
+    val A_types =
+      (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.DType t) | _ => I) A [];
     val typedef_deps = A_consts @ A_types;
 
     val newT_dep = Theory.DType (dest_Type newT);
diff -r 76148d288b2e -r 066792098895 src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Sep 22 15:58:19 2015 +0200
+++ b/src/Pure/term.ML	Tue Sep 22 16:17:49 2015 +0200
@@ -107,6 +107,7 @@
   val maxidx_of_typ: typ -> int
   val maxidx_of_typs: typ list -> int
   val maxidx_of_term: term -> int
+  val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   val exists_subtype: (typ -> bool) -> typ -> bool
   val exists_type: (typ -> bool) -> term -> bool
   val exists_subterm: (term -> bool) -> term -> bool
@@ -878,6 +879,12 @@
 
 (* substructure *)
 
+fun fold_subtypes f =
+  let
+    fun iter ty =
+      (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty);
+  in iter end;
+
 fun exists_subtype P =
   let
     fun ex ty = P ty orelse
diff -r 76148d288b2e -r 066792098895 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Sep 22 15:58:19 2015 +0200
+++ b/src/Pure/theory.ML	Tue Sep 22 16:17:49 2015 +0200
@@ -283,18 +283,18 @@
 
 local
 
-fun fold_type_constr f (Type (name, Ts)) = f (name,Ts) #> fold (fold_type_constr f) Ts
-  | fold_type_constr _ _ = I;
-
 fun check_def ctxt thy unchecked overloaded (b, tm) defs =
   let
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);
-    val rhs_consts = fold_aterms (fn Const const => insert (op =) (DConst const) | _ => I) rhs [];
-    val rhs_types = fold_types (fold_type_constr (insert (op =) o DType)) rhs []
-    val rhs_deps = rhs_consts @ rhs_types
+
+    val rhs_consts = fold_aterms (fn Const c => insert (op =) (DConst c) | _ => I) rhs [];
+    val rhs_types =
+      (fold_types o fold_subtypes) (fn Type t => insert (op =) (DType t) | _ => I) rhs [];
+    val rhs_deps = rhs_consts @ rhs_types;
+
     val _ = check_overloading ctxt overloaded lhs_const;
   in defs |> dependencies ctxt unchecked (SOME name) name (DConst lhs_const) rhs_deps end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block