--- a/LFex.thy	Thu Dec 03 02:53:54 2009 +0100
+++ b/LFex.thy	Thu Dec 03 11:28:19 2009 +0100
@@ -2,17 +2,17 @@
 imports Nominal QuotMain
 begin
 
-atom_decl name id
+atom_decl name ident
 
 nominal_datatype kind = 
     Type
   | KPi "ty" "name" "kind"
 and ty =  
-    TConst "id"
+    TConst "ident"
   | TApp "ty" "trm"
   | TPi "ty" "name" "ty"
 and trm = 
-    Const "id"
+    Const "ident"
   | Var "name"
   | App "trm" "trm"
   | Lam "ty" "name" "trm" 
@@ -93,7 +93,7 @@
   "KPI \<equiv> KPi"
 
 quotient_def 
-  TCONST :: "id \<Rightarrow> TY"
+  TCONST :: "ident \<Rightarrow> TY"
 where
   "TCONST \<equiv> TConst"
 
@@ -109,7 +109,7 @@
 
 (* FIXME: does not work with CONST *)
 quotient_def 
-  CONS :: "id \<Rightarrow> TRM"
+  CONS :: "ident \<Rightarrow> TRM"
 where
   "CONS \<equiv> Const"
 
@@ -264,6 +264,12 @@
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply - 
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
+(*
+Profiling:
+ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
+ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
+ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *}
+*)
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} quot defs 1 *})