reduced ML warnings;
authorwenzelm
Fri Feb 21 20:29:33 2014 +0100 (2014-02-21)
changeset 556594089f6e98ab9
parent 55656 eb07b0acbebc
child 55660 f0f895716a8b
reduced ML warnings;
src/HOL/Hoare/hoare_syntax.ML
src/HOL/Hoare/hoare_tac.ML
     1.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Fri Feb 21 18:23:11 2014 +0100
     1.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Fri Feb 21 20:29:33 2014 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  (*all meta-variables for bexp except for TRUE are translated as if they
     1.5    were boolean expressions*)
     1.6  
     1.7 -fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
     1.8 +fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE"   (* FIXME !? *)
     1.9    | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
    1.10  
    1.11  fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
    1.12 @@ -52,7 +52,7 @@
    1.13  
    1.14  fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
    1.15        Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
    1.16 -  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
    1.17 +  | com_tr (Const (@{const_syntax Basic},_) $ f) _ = Syntax.const @{const_syntax Basic} $ f
    1.18    | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
    1.19        Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
    1.20    | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
    1.21 @@ -88,27 +88,27 @@
    1.22    | dest_abstuple tm = tm;
    1.23  
    1.24  fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    1.25 -  | abs2list (Abs (x, T, t)) = [Free (x, T)]
    1.26 +  | abs2list (Abs (x, T, _)) = [Free (x, T)]
    1.27    | abs2list _ = [];
    1.28  
    1.29 -fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = mk_ts t
    1.30 -  | mk_ts (Abs (x, _, t)) = mk_ts t
    1.31 +fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t
    1.32 +  | mk_ts (Abs (_, _, t)) = mk_ts t
    1.33    | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
    1.34    | mk_ts t = [t];
    1.35  
    1.36  fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) =
    1.37        (Syntax.free x :: abs2list t, mk_ts t)
    1.38    | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
    1.39 -  | mk_vts t = raise Match;
    1.40 +  | mk_vts _ = raise Match;
    1.41  
    1.42 -fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
    1.43 +fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
    1.44    | find_ch ((v, t) :: vts) i xs =
    1.45        if t = Bound i then find_ch vts (i - 1) xs
    1.46        else (true, (v, subst_bounds (xs, t)));
    1.47  
    1.48 -fun is_f (Const (@{const_syntax case_prod}, _) $ Abs (x, _, t)) = true
    1.49 -  | is_f (Abs (x, _, t)) = true
    1.50 -  | is_f t = false;
    1.51 +fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true
    1.52 +  | is_f (Abs _) = true
    1.53 +  | is_f _ = false;
    1.54  
    1.55  
    1.56  (* assn_tr' & bexp_tr'*)
    1.57 @@ -148,7 +148,7 @@
    1.58  
    1.59  in
    1.60  
    1.61 -fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
    1.62 +fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q;
    1.63  
    1.64  end;
    1.65  
     2.1 --- a/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 18:23:11 2014 +0100
     2.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:29:33 2014 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4  
     2.5  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
     2.6  fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     2.7 -  | abs2list (Abs (x, T, t)) = [Free (x, T)]
     2.8 +  | abs2list (Abs (x, T, _)) = [Free (x, T)]
     2.9    | abs2list _ = [];
    2.10  
    2.11  (** maps {(x1,...,xn). t} to [x1,...,xn] **)
    2.12 @@ -115,7 +115,7 @@
    2.13  (** simplification done by (split_all_tac)                                  **)
    2.14  (*****************************************************************************)
    2.15  
    2.16 -fun set2pred_tac ctxt var_names = SUBGOAL (fn (goal, i) =>
    2.17 +fun set2pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
    2.18    before_set2pred_simp_tac ctxt i THEN_MAYBE
    2.19    EVERY [
    2.20      rtac subsetI i,
    2.21 @@ -175,6 +175,6 @@
    2.22  (** tac is the tactic the user chooses to solve or simplify **)
    2.23  (** the final verification conditions                       **)
    2.24  
    2.25 -fun hoare_tac ctxt (tac: int -> tactic) = SUBGOAL (fn (goal, i) =>
    2.26 +fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
    2.27    SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
    2.28