--- a/src/HOL/ex/Coercion_Examples.thy Fri Feb 22 20:12:53 2013 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy Fri Feb 22 20:25:51 2013 +0100
@@ -5,9 +5,11 @@
*)
theory Coercion_Examples
-imports Complex_Main
+imports Main
begin
+declare[[coercion_enabled]]
+
(* Error messages test *)
consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
--- a/src/Tools/subtyping.ML Fri Feb 22 20:12:53 2013 +0100
+++ b/src/Tools/subtyping.ML Fri Feb 22 20:25:51 2013 +0100
@@ -351,17 +351,18 @@
| INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx
handle NO_UNIFIER (msg, _) =>
err_list ctxt (gen_msg err
- "failed to unify invariant arguments w.r.t. to the known map function" ^ msg)
+ "failed to unify invariant arguments w.r.t. to the known map function\n" ^ msg)
(fst tye_idx) (T :: Ts))
| INVARIANT => (cs, strong_unify ctxt constraint tye_idx
handle NO_UNIFIER (msg, _) =>
- error (gen_msg err ("failed to unify invariant arguments" ^ msg))));
+ error (gen_msg err ("failed to unify invariant arguments\n" ^ msg))));
val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
(fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
val test_update = is_typeT orf is_freeT orf is_fixedvarT;
val (ch, done') =
- if not (null new) then ([], done)
- else split_cs (test_update o Type_Infer.deref tye') done;
+ done
+ |> map (apfst (pairself (Type_Infer.deref tye')))
+ |> (if not (null new) then rpair [] else split_cs test_update);
val todo' = ch @ todo;
in
simplify done' (new @ todo') (tye', idx')
@@ -505,7 +506,7 @@
(fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
handle NO_UNIFIER (msg, _) =>
err_bound ctxt
- (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
+ (gen_msg err ("constraint cycle not unifiable\n" ^ msg)) (fst tye_idx)
(find_cycle_packs cycle)))
cycles tye_idx
in