src/Pure/facts.ML
changeset 27175 620295a57106
parent 26692 3f48d4f4229f
child 27738 66596d7aa899
     1.1 --- a/src/Pure/facts.ML	Thu Jun 12 16:41:54 2008 +0200
     1.2 +++ b/src/Pure/facts.ML	Thu Jun 12 16:41:57 2008 +0200
     1.3 @@ -26,8 +26,8 @@
     1.4    val lookup: Context.generic -> T -> string -> thm list option
     1.5    val defined: T -> string -> bool
     1.6    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
     1.7 -  val dest_static: T -> (string * thm list) list
     1.8 -  val extern_static: T -> (xstring * thm list) list
     1.9 +  val dest_static: T list -> T -> (string * thm list) list
    1.10 +  val extern_static: T list -> T -> (xstring * thm list) list
    1.11    val props: T -> thm list
    1.12    val could_unify: T -> term -> thm list
    1.13    val merge: T * T -> T
    1.14 @@ -149,9 +149,19 @@
    1.15  
    1.16  fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
    1.17  
    1.18 -fun dest_static facts = sort_wrt #1 (fold_static cons facts []);
    1.19 -fun extern_static facts =
    1.20 -  sort_wrt #1 (fold_static (fn (name, ths) => cons (extern facts name, ths)) facts []);
    1.21 +
    1.22 +(* content difference *)
    1.23 +
    1.24 +fun diff_table prev_facts facts =
    1.25 +  fold_static (fn (name, ths) =>
    1.26 +    if exists (fn prev => defined prev name) prev_facts then I
    1.27 +    else cons (name, ths)) facts [];
    1.28 +
    1.29 +fun dest_static prev_facts facts =
    1.30 +  sort_wrt #1 (diff_table prev_facts facts);
    1.31 +
    1.32 +fun extern_static prev_facts facts =
    1.33 +  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts)));
    1.34  
    1.35  
    1.36  (* indexed props *)
    1.37 @@ -166,6 +176,7 @@
    1.38  
    1.39  fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
    1.40  
    1.41 +(* FIXME stamp identity! *)
    1.42  fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
    1.43    | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
    1.44