# HG changeset patch # User wenzelm # Date 1440929843 -7200 # Node ID 408ff239053085172c9ab1399205813157514f75 # Parent bf05dc1a77c0e56b6e7834582ed2ff1788203d81 trim context for persistent storage; diff -r bf05dc1a77c0 -r 408ff2390530 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Aug 30 11:56:37 2015 +0200 +++ b/src/Pure/thm.ML Sun Aug 30 12:17:23 2015 +0200 @@ -34,6 +34,7 @@ val maxidx_of_cterm: cterm -> int val global_cterm_of: theory -> term -> cterm val cterm_of: Proof.context -> term -> cterm + val trim_context_cterm: cterm -> cterm val transfer_cterm: theory -> cterm -> cterm val renamed_term: term -> cterm -> cterm val dest_comb: cterm -> cterm * cterm @@ -76,6 +77,7 @@ val cprop_of: thm -> cterm val cprem_of: thm -> int -> cterm val chyps_of: thm -> cterm list + val trim_context: thm -> thm val transfer: theory -> thm -> thm val renamed_prop: term -> thm -> thm val weaken: cterm -> thm -> thm @@ -196,6 +198,13 @@ fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) = Context.join_certificate (cert1, cert2); +fun trim_context_cterm ct = + (case ct of + Cterm {cert = Context.Certificate_Id _, ...} => ct + | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} => + Cterm {cert = Context.Certificate_Id (Context.theory_id thy), + t = t, T = T, maxidx = maxidx, sorts = sorts}); + fun transfer_cterm thy' ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; @@ -437,7 +446,14 @@ fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps; -(*explicit transfer to a super theory*) +fun trim_context th = + (case th of + Thm (_, {cert = Context.Certificate_Id _, ...}) => th + | Thm (der, {cert = Context.Certificate thy, tags, maxidx, shyps, hyps, tpairs, prop}) => + Thm (der, + {cert = Context.Certificate_Id (Context.theory_id thy), + tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})); + fun transfer thy' thm = let val Thm (der, {cert, tags, maxidx, shyps, hyps, tpairs, prop}) = thm;