--- a/Nominal/Ex/SingleLet.thy	Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Mon Aug 16 17:39:16 2010 +0800
@@ -22,6 +22,7 @@
   "bn (As x y t) = {atom x}"
 
 (* can lift *)
+
 thm distinct
 thm trm_raw_assg_raw.inducts
 thm fv_defs
@@ -57,7 +58,18 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
 *}
 
-
+ML {*
+  Local_Theory.exit_global;
+  Class.instantiation;
+  Class.prove_instantiation_exit_result;
+  Named_Target.theory_init;
+  op |->
+*}
+  
+done
+|> ...
+  |-> (fn x => Class.prove_instantiation_exit_result phi tac x)
+  |-> (fn y => ...)
 
 
 
@@ -87,35 +99,6 @@
   val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
 *}
 
-section {* NOT *}
-
-ML {*
-  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
-*}
-
-instance trm :: pt sorry
-instance assg :: pt sorry
-
-
-
-
-
-
-
-
-
-
-thm eq_iff[no_vars]
-
-ML {*
-  val q1 = lift_thm [@{typ trm}, @{typ assg}] @{context} @{thm "eq_iff"(1)}
-*}
-
-local_setup {* Local_Theory.note ((@{binding d1}, []), thms_d) #> snd *}
-local_setup {* Local_Theory.note ((@{binding i1}, []), thms_i) #> snd *}
-local_setup {* Local_Theory.note ((@{binding f1}, []), thms_f) #> snd *}
-local_setup {* Local_Theory.note ((@{binding q1}, []), [q1]) #> snd *}
-
 
 thm perm_defs
 thm perm_simps
@@ -139,27 +122,6 @@
 
 
 
-ML {*
-  map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff}
-*}
-
-
-
-
-
-lemma "Var x \<noteq> App y1 y2"
-apply(descending)
-apply(simp add: trm_raw.distinct)
-
-
-
-ML {*
-  map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.distinct(1)}
-*}
-
-
-
-
 typ trm
 typ assg