merged

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 05 16:23:51 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 05 17:36:15 2009 +0100
@@ -546,9 +546,9 @@
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
   val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
   val intro = Goal.prove (ProofContext.init thy) names [] intro_t
-        (fn {...} => etac @{thm FalseE} 1)
+        (fn _ => etac @{thm FalseE} 1)
   val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
-        (fn {...} => etac elim 1) 
+        (fn _ => etac elim 1) 
 in
   ([intro], elim)
 end
@@ -1440,10 +1440,14 @@
   val simprules = [defthm, @{thm eval_pred},
     @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
-  val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
+  val introthm =
+    Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm
+      (fn _ => unfolddef_tac)
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
-  val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
+  val elimthm =
+    Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm
+      (fn _ => unfolddef_tac)
 in
   (introthm, elimthm)
 end;
@@ -2157,7 +2161,7 @@
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
             val def = predfun_definition_of thy predname full_mode
-            val tac = fn {...} => Simplifier.simp_tac
+            val tac = fn _ => Simplifier.simp_tac
               (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
             val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
           in

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Nov 05 16:23:51 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Nov 05 17:36:15 2009 +0100
@@ -113,7 +113,7 @@
     val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
     val t' = Pattern.rewrite_term thy rewr [] t
     val tac = Skip_Proof.cheat_tac thy
-    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
+    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
     val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
   in
     th'''

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Nov 05 16:23:51 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Nov 05 17:36:15 2009 +0100
@@ -98,7 +98,7 @@
               THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
               THEN TRY (atac 1)
           in
-            Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
+            Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac)
           end
       in
         map_index prove_introrule (map mk_introrule disjuncts)

--- a/src/HOLCF/Tools/adm_tac.ML	Thu Nov 05 16:23:51 2009 +0100
+++ b/src/HOLCF/Tools/adm_tac.ML	Thu Nov 05 17:36:15 2009 +0100
@@ -1,4 +1,5 @@
-(*  Author:     Stefan Berghofer, TU Muenchen
+(*  Title:      HOLCF/Tools/adm_tac.ML
+    Author:     Stefan Berghofer, TU Muenchen
 
 Admissibility tactic.
 
@@ -18,7 +19,7 @@
   val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end;
 
-structure Adm :> ADM =
+structure Adm : ADM =
 struct
 
 

--- a/src/HOLCF/Tools/fixrec.ML	Thu Nov 05 16:23:51 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Thu Nov 05 17:36:15 2009 +0100
@@ -13,8 +13,8 @@
   val add_fixpat: Thm.binding * term list -> theory -> theory
   val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
   val add_matchers: (string * string) list -> theory -> theory
-  val fixrec_simp_add: Thm.attribute
-  val fixrec_simp_del: Thm.attribute
+  val fixrec_simp_add: attribute
+  val fixrec_simp_del: attribute
   val fixrec_simp_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
 end;
@@ -165,7 +165,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  val merge = K (Symtab.merge (K true));
+  fun merge _ = Symtab.merge (K true);
 );
 
 local
@@ -179,7 +179,7 @@
 
 in
 
-val add_unfold : Thm.attribute =
+val add_unfold : attribute =
   Thm.declaration_attribute
     (fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th)));
 
@@ -257,7 +257,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  val merge = K (Symtab.merge (K true));
+  fun merge _ = Symtab.merge (K true);
 );
 
 (* associate match functions with pattern constants *)
@@ -372,7 +372,7 @@
       addsimprocs [@{simproc cont_proc}];
   val copy = I;
   val extend = I;
-  val merge = K merge_ss;
+  fun merge _ = merge_ss;
 );
 
 fun fixrec_simp_tac ctxt =
@@ -391,14 +391,14 @@
         CHANGED (rtac rule i THEN asm_simp_tac ss i)
       end
   in
-    SUBGOAL (fn ti => tac ti handle _ => no_tac)
+    SUBGOAL (fn ti => tac ti handle _ => no_tac)  (* FIXME avoid handle _ *)
   end;
 
-val fixrec_simp_add : Thm.attribute =
+val fixrec_simp_add : attribute =
   Thm.declaration_attribute
     (fn th => FixrecSimpData.map (fn ss => ss addsimps [th]));
 
-val fixrec_simp_del : Thm.attribute =
+val fixrec_simp_del : attribute =
   Thm.declaration_attribute
     (fn th => FixrecSimpData.map (fn ss => ss delsimps [th]));