src/HOL/Hoare/hoare_tac.ML
changeset 55659 4089f6e98ab9
parent 55414 eab03e9cee8a
child 55660 f0f895716a8b
--- 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);