--- 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
--- 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
--- 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)
--- 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) [];
--- 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;