reduced ML warnings;

--- a/src/HOL/Hoare/hoare_syntax.ML	Fri Feb 21 18:23:11 2014 +0100
+++ b/src/HOL/Hoare/hoare_syntax.ML	Fri Feb 21 20:29:33 2014 +0100
@@ -42,7 +42,7 @@
 (*all meta-variables for bexp except for TRUE are translated as if they
   were boolean expressions*)
 
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
+fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE"   (* FIXME !? *)
   | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
 
 fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
@@ -52,7 +52,7 @@
 
 fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
       Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
-  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+  | com_tr (Const (@{const_syntax Basic},_) $ f) _ = Syntax.const @{const_syntax Basic} $ f
   | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
       Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
   | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
@@ -88,27 +88,27 @@
   | dest_abstuple tm = tm;
 
 fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
-  | abs2list (Abs (x, T, t)) = [Free (x, T)]
+  | abs2list (Abs (x, T, _)) = [Free (x, T)]
   | abs2list _ = [];
 
-fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = mk_ts t
-  | mk_ts (Abs (x, _, t)) = mk_ts t
+fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t
+  | mk_ts (Abs (_, _, t)) = mk_ts t
   | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
   | mk_ts t = [t];
 
 fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
       (Syntax.free x :: abs2list t, mk_ts t)
   | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
-  | mk_vts t = raise Match;
+  | mk_vts _ = raise Match;
 
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
+fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
   | find_ch ((v, t) :: vts) i xs =
       if t = Bound i then find_ch vts (i - 1) xs
       else (true, (v, subst_bounds (xs, t)));
 
-fun is_f (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = true
-  | is_f (Abs (x, _, t)) = true
-  | is_f t = false;
+fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
+  | is_f (Abs _) = true
+  | is_f _ = false;
 
 
 (* assn_tr' & bexp_tr'*)
@@ -148,7 +148,7 @@
 
 in
 
-fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
+fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q;
 
 end;
 

--- a/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 18:23:11 2014 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:29:33 2014 +0100
@@ -19,7 +19,7 @@
 
 (** maps (%x1 ... xn. t) to [x1,...,xn] **)
 fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
-  | abs2list (Abs (x, T, t)) = [Free (x, T)]
+  | abs2list (Abs (x, T, _)) = [Free (x, T)]
   | abs2list _ = [];
 
 (** maps {(x1,...,xn). t} to [x1,...,xn] **)
@@ -115,7 +115,7 @@
 (** simplification done by (split_all_tac)                                  **)
 (*****************************************************************************)
 
-fun set2pred_tac ctxt var_names = SUBGOAL (fn (goal, i) =>
+fun set2pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
   before_set2pred_simp_tac ctxt i THEN_MAYBE
   EVERY [
     rtac subsetI i,
@@ -175,6 +175,6 @@
 (** tac is the tactic the user chooses to solve or simplify **)
 (** the final verification conditions                       **)
 
-fun hoare_tac ctxt (tac: int -> tactic) = SUBGOAL (fn (goal, i) =>
+fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
   SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);