--- a/src/Tools/subtyping.ML Tue Apr 19 16:13:04 2011 +0200
+++ b/src/Tools/subtyping.ML Tue Apr 19 20:47:02 2011 +0200
@@ -516,8 +516,8 @@
| SOME S =>
SOME
(map nameT
- (filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))),
- S));
+ (filter_out Type_Infer.is_paramT
+ (map (Type_Infer.deref tye) (get_bound G T))), S));
val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound);
val assignment =
if null bound orelse null not_params then NONE
@@ -647,7 +647,8 @@
end
| insert bs (t $ u) =
let
- val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t);
+ val (t', Type ("fun", [U, T])) =
+ apsnd (Type_Infer.deref tye) (insert bs t);
val (u', U') = insert bs u;
in
if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U')
@@ -664,10 +665,7 @@
fun coercion_infer_types ctxt raw_ts =
let
- val const_type = try (Consts.the_constraint (Proof_Context.consts_of ctxt));
- val var_type = Proof_Context.def_type ctxt;
-
- val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
+ val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts;
fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
| inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)