# HG changeset patch
# User wenzelm
# Date 1331556806 -3600
# Node ID 7a73f181cbcfd53ced00874b57825c629b626a4b
# Parent  bad72cba8a92030ae308f7af689e3acfe4a382fe
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;

diff -r bad72cba8a92 -r 7a73f181cbcf src/Pure/type_infer_context.ML
--- 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 =