--- 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);
--- 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
--- 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