src/Provers/classical.ML

 val claset_of = claset_of_sg o sign_of;
 
 fun CLASET tacf state = tacf (claset_of_sg (sign_of_thm state)) state;
 fun CLASET' tacf i state = tacf (claset_of_sg (sign_of_thm state)) i state;
 
-val claset = claset_of o Context.get_context;
-val claset_ref = claset_ref_of_sg o sign_of o Context.get_context;
+val claset = claset_of o Context.the_context;
+val claset_ref = claset_ref_of_sg o sign_of o Context.the_context;
 
 
 (* change claset *)
 
 fun change_claset f x = claset_ref () := (f (claset (), x));