clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
authorwenzelm
Mon, 12 Mar 2012 13:53:26 +0100
changeset 46873 7a73f181cbcf
parent 46872 bad72cba8a92
child 46874 993c413746f4
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
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 =