Lines Matching defs:seg
304 fun makeCT seg = CT := seg
383 fun add_fact (th as (s,_)) (seg : segment) =
384 update_seg seg (U #facts (overwrite th (#facts seg))) $$
392 fun add_ML_dep s (seg as {mldeps, ...} : segment) =
393 update_seg seg (U #mldeps (HOLset.add(mldeps, s))) $$
402 fun set_MLbind (s1,s2) (seg as {facts, ...} : segment) =
405 seg)
407 update_seg seg (U #facts (X@((s2,b)::Y))) $$
817 val (seg as {thydata,...}) = theCT()
819 makeCT (update_seg seg (U #thydata (update1 thydata)) $$)