--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/progtut/Advanced.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,46 @@
+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