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