moved RANGE to tctical.ML;
moved export_assume, export_presume, export_def to proof_context.ML;
consts assoc :: "('key * 'val)list => 'key => 'val option"
primrec "assoc [] x = None"
"assoc (p#ps) x =
(let (a,b) = p in if a=x then Some b else assoc ps x)"