theory Advanced
imports Essential
begin

lemma "True"
proof -
  ML_prf {* Variable.dest_fixes @{context} *}
  fix x y
  ML_prf {* Variable.dest_fixes @{context} *}
  show ?thesis by auto
qed

lemma "True"
proof -
  fix x y
  { fix z w
    ML_prf {* Variable.dest_fixes @{context} *}
  }
  ML_prf {* Variable.dest_fixes @{context} *}
  show ?thesis by auto
qed

ML {*
val ctxt0 = @{context};
val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;
val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1;
val trm = @{term "(x, y, z, w)"};

  pwriteln (Pretty.chunks
    [ pretty_term ctxt0 trm,
      pretty_term ctxt1 trm,
      pretty_term ctxt2 trm ])
*}

ML {*
  let
     val ctxt0 = @{context}
     val (y, ctxt1) = Variable.add_fixes ["x"] ctxt0
     val frees = replicate 2 ("x", @{typ nat})
  in
     (Variable.variant_frees ctxt0 [] frees,
      Variable.variant_frees ctxt1 [] frees, y)
  end
*}

end