clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
--- a/src/Pure/type_infer_context.ML Sun Mar 11 22:06:13 2012 +0100
+++ b/src/Pure/type_infer_context.ML Mon Mar 12 13:53:26 2012 +0100
@@ -118,18 +118,14 @@
fun prepare_positions ctxt tms =
let
- val visible = Context_Position.is_visible ctxt;
-
fun prepareT (Type (a, Ts)) ps_idx =
let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx
in (Type (a, Ts'), ps_idx') end
| prepareT T (ps, idx) =
(case Term_Position.decode_positionT T of
SOME pos =>
- if visible then
- let val U = Type_Infer.mk_param idx []
- in (U, ((pos, U) :: ps, idx + 1)) end
- else (dummyT, (ps, idx))
+ let val U = Type_Infer.mk_param idx []
+ in (U, ((pos, U) :: ps, idx + 1)) end
| NONE => (T, (ps, idx)));
fun prepare (Const ("_type_constraint_", T)) ps_idx =