--- a/FSet.thy	Thu Oct 29 07:29:12 2009 +0100
+++ b/FSet.thy	Thu Oct 29 08:06:49 2009 +0100
@@ -177,7 +177,7 @@
 term fmap
 thm fmap_def
 
-ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def card_def INSERT_def fmap_def fold_def} *}
+ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *}
 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 
 ML {*
@@ -187,7 +187,6 @@
                 @{const_name "map"}];
 *}
 
-(* FIXME: does not work anymore :o( *)
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
 lemma memb_rsp:
@@ -315,7 +314,7 @@
   @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *}
 ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *}
-ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+ML {* val defs = fset_defs *}
 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},

--- a/LamEx.thy	Thu Oct 29 07:29:12 2009 +0100
+++ b/LamEx.thy	Thu Oct 29 08:06:49 2009 +0100
@@ -17,7 +17,6 @@
 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 quotient lam = rlam / alpha
-apply -
 sorry
 
 print_quotients

--- a/isar-keywords-prove.el	Thu Oct 29 07:29:12 2009 +0100
+++ b/isar-keywords-prove.el	Thu Oct 29 08:06:49 2009 +0100
@@ -335,6 +335,7 @@
     "header"
     "help"
     "kill_thy"
+    "nitpick"
     "normal_form"
     "pr"
     "pretty_setmargin"
@@ -581,7 +582,6 @@
     "apply_end"
     "back"
     "defer"
-    "nitpick"
     "prefer"))
 
 (provide 'isar-keywords)