added pos_of_ref;
authorwenzelm
Thu Mar 20 17:38:53 2008 +0100 (2008-03-20)
changeset 263665c089f4219c2
parent 26365 e6d3714b8853
child 26367 06635166d211
added pos_of_ref;
src/Pure/facts.ML
     1.1 --- a/src/Pure/facts.ML	Thu Mar 20 16:54:11 2008 +0100
     1.2 +++ b/src/Pure/facts.ML	Thu Mar 20 17:38:53 2008 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    val named: string -> ref
     1.5    val string_of_ref: ref -> string
     1.6    val name_of_ref: ref -> string
     1.7 +  val pos_of_ref: ref -> Position.T
     1.8    val map_name_of_ref: (string -> string) -> ref -> ref
     1.9    val select: ref -> thm list -> thm list
    1.10    val selections: string * thm list -> (ref * thm) list
    1.11 @@ -69,8 +70,11 @@
    1.12  
    1.13  fun named name = Named ((name, Position.none), NONE);
    1.14  
    1.15 -fun name_of_ref (Named ((name, _), _)) = name
    1.16 -  | name_of_ref (Fact _) = error "Illegal literal fact";
    1.17 +fun name_pos_of_ref (Named (name_pos, _)) = name_pos
    1.18 +  | name_pos_of_ref (Fact _) = error "Illegal literal fact";
    1.19 +
    1.20 +val name_of_ref = #1 o name_pos_of_ref;
    1.21 +val pos_of_ref = #2 o name_pos_of_ref;
    1.22  
    1.23  fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    1.24    | map_name_of_ref _ r = r;