--- a/Nominal/Ex/SingleLet.thy	Sun Aug 15 11:03:13 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 15 14:00:28 2010 +0800
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 18]]
+declare [[STEPS = 20]]
 
 nominal_datatype trm  =
   Var "name"
@@ -33,44 +33,6 @@
 thm eq_iff
 thm eq_iff_simps
 
-instantiation trm and assg :: size 
-begin
-
-quotient_definition 
-  "size_trm :: trm \<Rightarrow> nat"
-is "size :: trm_raw \<Rightarrow> nat"
-
-quotient_definition 
-  "size_assg :: assg \<Rightarrow> nat"
-is "size :: assg_raw \<Rightarrow> nat"
-
-instance .. 
-
-end 
-
-instantiation trm and assg :: pt
-begin
-
-quotient_definition 
-  "permute_trm :: perm => trm => trm" 
-  is "permute :: perm \<Rightarrow> trm_raw \<Rightarrow> trm_raw"
-
-quotient_definition 
-  "permute_assg :: perm => assg => assg" 
-  is "permute :: perm \<Rightarrow> assg_raw \<Rightarrow> assg_raw"
-
-lemma qperm_laws:
-  fixes t::trm and a::assg
-  shows "permute 0 t = t"
-  and   "permute 0 a = a" 
-sorry
-  
-instance
-apply(default)
-sorry
-
-end
-
 ML {*
   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
 *}