# HG changeset patch
# User wenzelm
# Date 1254429629 -7200
# Node ID 98702c579ad0f62b7349a840c0e0043facc78b38
# Parent  57dcddf81b01dcb010f576671b7fb0083b78d790
added Ctermtab, cterm_cache, thm_cache;
tuned;

diff -r 57dcddf81b01 -r 98702c579ad0 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Oct 01 22:39:58 2009 +0200
+++ b/src/Pure/more_thm.ML	Thu Oct 01 22:40:29 2009 +0200
@@ -6,9 +6,19 @@
 
 infix aconvc;
 
+signature BASIC_THM =
+sig
+  include BASIC_THM
+  structure Ctermtab: TABLE
+  structure Thmtab: TABLE
+  val aconvc: cterm * cterm -> bool
+end;
+
 signature THM =
 sig
   include THM
+  structure Ctermtab: TABLE
+  structure Thmtab: TABLE
   val aconvc: cterm * cterm -> bool
   val add_cterm_frees: cterm -> cterm list -> cterm list
   val all_name: string * cterm -> cterm -> cterm
@@ -22,6 +32,8 @@
   val lhs_of: thm -> cterm
   val rhs_of: thm -> cterm
   val thm_ord: thm * thm -> order
+  val cterm_cache: (cterm -> 'a) -> cterm -> 'a
+  val thm_cache: (thm -> 'a) -> thm -> 'a
   val is_reflexive: thm -> bool
   val eq_thm: thm * thm -> bool
   val eq_thms: thm list * thm list -> bool
@@ -163,6 +175,15 @@
   end;
 
 
+(* tables and caches *)
+
+structure Ctermtab = Table(type key = cterm val ord = TermOrd.fast_term_ord o pairself Thm.term_of);
+structure Thmtab = Table(type key = thm val ord = thm_ord);
+
+fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;
+fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f;
+
+
 (* equality *)
 
 fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
@@ -432,6 +453,6 @@
 
 end;
 
-val op aconvc = Thm.aconvc;
+structure Basic_Thm: BASIC_THM = Thm;
+open Basic_Thm;
 
-structure Thmtab = Table(type key = thm val ord = Thm.thm_ord);