--- a/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 15:05:59 2009 +0100
@@ -75,7 +75,7 @@
let
fun mk_branch concl =
let
- val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+ val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
val (P, xs) = strip_comb Pxs
in
SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
@@ -103,7 +103,7 @@
fun mk_rcinfo pr =
let
- val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+ val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
val (P', rcs) = strip_comb Phyp
in
(bidx P', Gvs, Gas, rcs)
@@ -151,7 +151,7 @@
|> mk_forall_rename ("P", Pbool)
end
-fun mk_wf ctxt R (IndScheme {T, ...}) =
+fun mk_wf R (IndScheme {T, ...}) =
HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
fun mk_ineqs R (IndScheme {T, cases, branches}) =
@@ -198,8 +198,6 @@
end
-fun mk_hol_imp a b = HOLogic.imp $ a $ b
-
fun mk_ind_goal thy branches =
let
fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
@@ -256,7 +254,7 @@
val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
|> split_list
- fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
+ fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
let
val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
@@ -364,7 +362,7 @@
val ineqss = mk_ineqs R scheme
|> map (map (pairself (assume o cert)))
val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
- val wf_thm = mk_wf ctxt R scheme |> cert |> assume
+ val wf_thm = mk_wf R scheme |> cert |> assume
val (descent, pres) = split_list (flat ineqss)
val newgoals = complete @ pres @ wf_thm :: descent