--- a/src/Pure/facts.ML Tue Jun 21 11:03:24 2016 +0200
+++ b/src/Pure/facts.ML Tue Jun 21 14:42:47 2016 +0200
@@ -36,8 +36,8 @@
val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
val dest_static: bool -> T list -> T -> (string * thm list) list
val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
- val props: T -> thm list
- val could_unify: T -> term -> thm list
+ val props: T -> (thm * Position.T) list
+ val could_unify: T -> term -> (thm * Position.T) list
val merge: T * T -> T
val add_static: Context.generic -> {strict: bool, index: bool} ->
binding * thm list -> T -> string * T
@@ -134,7 +134,7 @@
datatype T = Facts of
{facts: fact Name_Space.table,
- props: thm Net.net};
+ props: (thm * Position.T) Net.net};
fun make_facts facts props = Facts {facts = facts, props = props};
@@ -227,7 +227,7 @@
(* indexed props *)
-val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of;
+val prop_ord = Term_Ord.term_ord o apply2 (Thm.full_prop_of o fst);
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
fun could_unify (Facts {props, ...}) = Net.unify_term props;
@@ -250,11 +250,13 @@
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
let
val ths' = map Thm.trim_context ths;
+ val pos = #2 (Position.default (Binding.pos_of b));
+
val (name, facts') =
if Binding.is_empty b then ("", facts)
else Name_Space.define context strict (b, Static ths') facts;
val props' = props
- |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths';
+ |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths';
in (name, make_facts facts' props') end;