# HG changeset patch
# User wenzelm
# Date 1393324564 -3600
# Node ID 11dd48f84441b5b01d2273d25d3a4f807be2e4a7
# Parent  d8270c17b5beffb0eb9e88690156893139c04420
more positions;
tuned messages;

diff -r d8270c17b5be -r 11dd48f84441 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Feb 25 10:50:12 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Feb 25 11:36:04 2014 +0100
@@ -231,7 +231,7 @@
       let
         val atts = map (attribute_generic context) srcs;
         val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
-      in (context', pick "" [th']) end)
+      in (context', pick ("", Position.none) [th']) end)
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
       >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
@@ -244,7 +244,7 @@
         val atts = map (attribute_generic context) srcs;
         val (ths', context') =
           fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
-      in (context', pick name ths') end)
+      in (context', pick (name, Facts.pos_of_ref thmref) ths') end)
   end);
 
 in
diff -r d8270c17b5be -r 11dd48f84441 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Feb 25 10:50:12 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Feb 25 11:36:04 2014 +0100
@@ -933,7 +933,7 @@
             [res] => res
           | [] => err "Failed to retrieve literal fact"
           | _ => err "Ambiguous specification of literal fact");
-      in pick "" [res] end
+      in pick ("", Position.none) [res] end
   | retrieve_thms pick ctxt xthmref =
       let
         val thy = theory_of ctxt;
@@ -950,7 +950,7 @@
                   (Name_Space.markup (Facts.space_of local_facts) name);
                  map (Thm.transfer thy) (Facts.select thmref ths))
             | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
-      in pick name thms end;
+      in pick (name, pos) thms end;
 
 in
 
diff -r d8270c17b5be -r 11dd48f84441 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Tue Feb 25 10:50:12 2014 +0100
+++ b/src/Pure/facts.ML	Tue Feb 25 11:36:04 2014 +0100
@@ -6,7 +6,7 @@
 
 signature FACTS =
 sig
-  val the_single: string -> thm list -> thm
+  val the_single: string * Position.T -> thm list -> thm
   datatype interval = FromTo of int * int | From of int | Single of int
   datatype ref =
     Named of (string * Position.T) * interval list option |
@@ -46,7 +46,9 @@
 (** fact references **)
 
 fun the_single _ [th] : thm = th
-  | the_single name _ = error ("Expected singleton fact " ^ quote name);
+  | the_single (name, pos) ths =
+      error ("Expected singleton fact " ^ quote name ^
+        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
 
 
 (* datatype interval *)
@@ -77,12 +79,15 @@
 
 fun named name = Named ((name, Position.none), NONE);
 
+fun name_of_ref (Named ((name, _), _)) = name
+  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
+
+fun pos_of_ref (Named ((_, pos), _)) = pos
+  | pos_of_ref (Fact _) = Position.none;
+
 fun name_pos_of_ref (Named (name_pos, _)) = name_pos
   | name_pos_of_ref (Fact _) = raise Fail "Illegal literal fact";
 
-val name_of_ref = #1 o name_pos_of_ref;
-val pos_of_ref = #2 o name_pos_of_ref;
-
 fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
   | map_name_of_ref _ r = r;
 
@@ -101,7 +106,7 @@
       let
         val n = length ths;
         fun err msg =
-          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
+          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
             Position.here pos);
         fun sel i =
           if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
diff -r d8270c17b5be -r 11dd48f84441 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Tue Feb 25 10:50:12 2014 +0100
+++ b/src/Pure/global_theory.ML	Tue Feb 25 11:36:04 2014 +0100
@@ -86,7 +86,7 @@
   end;
 
 fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
-fun get_thm thy name = Facts.the_single name (get_thms thy name);
+fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name);
 
 fun all_thms_of thy =
   Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
diff -r d8270c17b5be -r 11dd48f84441 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Tue Feb 25 10:50:12 2014 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Tue Feb 25 11:36:04 2014 +0100
@@ -166,8 +166,8 @@
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
-    val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
+    val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]);
+    val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]);
     val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
     val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
   in rep_datatype_i elim induct case_eqns recursor_eqns thy end;