discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Simplifier and equational conversions demand a proper proof context;
(*:maxLineLen=78:*)
theory Base
imports Main
begin
ML_file \<open>../antiquote_setup.ML\<close>
end