--- a/src/HOL/Tools/split_rule.ML Sun Sep 28 20:27:46 2014 +0200
+++ b/src/HOL/Tools/split_rule.ML Sun Sep 28 20:27:47 2014 +0200
@@ -37,7 +37,7 @@
ap_split T2 T3
((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
Bound 0))
- | ap_split T T3 u = u;
+ | ap_split _ T3 u = u;
(*Curries any Var of function type in the rule*)
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
@@ -45,7 +45,7 @@
val newt = ap_split T1 T2 (Var (v, T'));
val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
- | split_rule_var' t rl = rl;
+ | split_rule_var' _ rl = rl;
(* complete splitting of partially split rules *)
@@ -82,7 +82,7 @@
| collect_vars t =
(case strip_comb t of
(v as Var _, ts) => cons (v, ts)
- | (t, ts) => fold collect_vars ts);
+ | (_, ts) => fold collect_vars ts);
fun split_rule_var ctxt =