src/Pure/facts.ML
changeset 55740 11dd48f84441
parent 49887 1a173b2503c0
child 56003 eccac152ffb4
     1.1 --- a/src/Pure/facts.ML	Tue Feb 25 10:50:12 2014 +0100
     1.2 +++ b/src/Pure/facts.ML	Tue Feb 25 11:36:04 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature FACTS =
     1.6  sig
     1.7 -  val the_single: string -> thm list -> thm
     1.8 +  val the_single: string * Position.T -> thm list -> thm
     1.9    datatype interval = FromTo of int * int | From of int | Single of int
    1.10    datatype ref =
    1.11      Named of (string * Position.T) * interval list option |
    1.12 @@ -46,7 +46,9 @@
    1.13  (** fact references **)
    1.14  
    1.15  fun the_single _ [th] : thm = th
    1.16 -  | the_single name _ = error ("Expected singleton fact " ^ quote name);
    1.17 +  | the_single (name, pos) ths =
    1.18 +      error ("Expected singleton fact " ^ quote name ^
    1.19 +        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
    1.20  
    1.21  
    1.22  (* datatype interval *)
    1.23 @@ -77,12 +79,15 @@
    1.24  
    1.25  fun named name = Named ((name, Position.none), NONE);
    1.26  
    1.27 +fun name_of_ref (Named ((name, _), _)) = name
    1.28 +  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
    1.29 +
    1.30 +fun pos_of_ref (Named ((_, pos), _)) = pos
    1.31 +  | pos_of_ref (Fact _) = Position.none;
    1.32 +
    1.33  fun name_pos_of_ref (Named (name_pos, _)) = name_pos
    1.34    | name_pos_of_ref (Fact _) = raise Fail "Illegal literal fact";
    1.35  
    1.36 -val name_of_ref = #1 o name_pos_of_ref;
    1.37 -val pos_of_ref = #2 o name_pos_of_ref;
    1.38 -
    1.39  fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    1.40    | map_name_of_ref _ r = r;
    1.41  
    1.42 @@ -101,7 +106,7 @@
    1.43        let
    1.44          val n = length ths;
    1.45          fun err msg =
    1.46 -          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    1.47 +          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    1.48              Position.here pos);
    1.49          fun sel i =
    1.50            if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)