--- a/src/HOL/Tools/typedef.ML Tue Sep 22 14:32:23 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Tue Sep 22 15:58:19 2015 +0200
@@ -132,14 +132,14 @@
|> Local_Theory.background_theory_result
(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_types = fold_types (fold_type_constr (insert (op =) o Theory.DType)) A [];
val typedef_deps = A_consts @ A_types;
-
+
val newT_dep = Theory.DType (dest_Type newT);
val ((axiom_name, axiom), axiom_lthy) = consts_lthy