--- a/src/Pure/Syntax/term_position.ML Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/Syntax/term_position.ML Thu Nov 10 22:32:10 2011 +0100
@@ -9,7 +9,8 @@
val pretty: Position.T -> Pretty.T
val encode: Position.T -> string
val decode: string -> Position.T option
- val decode_position: term -> Position.T option
+ val decode_position: term -> (Position.T * typ) option
+ val decode_positionT: typ -> Position.T option
val is_position: term -> bool
val strip_positions: term -> term
end;
@@ -39,9 +40,15 @@
(* positions within parse trees *)
-fun decode_position (Free (x, _)) = decode x
+fun decode_position (Free (x, _)) =
+ (case decode x of
+ SOME pos => SOME (pos, TFree (x, dummyS))
+ | NONE => NONE)
| decode_position _ = NONE;
+fun decode_positionT (TFree (x, _)) = decode x
+ | decode_positionT _ = NONE;
+
val is_position = is_some o decode_position;
fun strip_positions ((t as Const (c, _)) $ u $ v) =