1.1 --- a/src/HOL/Tools/Function/function_elims.ML	Fri Dec 13 13:59:01 2013 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_elims.ML	Fri Dec 13 14:09:51 2013 +0100
     1.3 @@ -53,13 +53,13 @@
     1.4      asm_lr_simp_tac ss i thm
     1.5    end;
     1.6  
     1.7 -val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+};
     1.8 +val eq_boolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+};
     1.9  val boolE = @{thms HOL.TrueE HOL.FalseE};
    1.10  val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+};
    1.11 -val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False};
    1.12 +val eq_bool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False};
    1.13  
    1.14  fun bool_subst_tac ctxt i =
    1.15 -  REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
    1.16 +  REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i)
    1.17    THEN REPEAT (dresolve_tac boolD i)
    1.18    THEN REPEAT (eresolve_tac boolE i)
    1.19  
    1.20 @@ -69,7 +69,7 @@
    1.21      fun mk_bool_elim b =
    1.22        elim
    1.23        |> Thm.forall_elim b
    1.24 -      |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
    1.25 +      |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eq_boolI 1))
    1.26        |> Tactic.rule_by_tactic ctxt tac;
    1.27    in
    1.28      map mk_bool_elim [@{cterm True}, @{cterm False}]
    1.29 @@ -81,8 +81,7 @@
    1.30    let
    1.31      val thy = Proof_Context.theory_of ctxt;
    1.32  
    1.33 -    val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
    1.34 -      termination, domintros, ...} = result;
    1.35 +    val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
    1.36      val n_fs = length fs;
    1.37  
    1.38      fun mk_partial_elim_rule (idx, f) =
    1.39 @@ -93,7 +92,7 @@
    1.40            | mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
    1.41                let val xn = Free ("x" ^ Int.toString n, S)
    1.42                in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end
    1.43 -          | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]));
    1.44 +          | mk_funeq _ _ _ = raise TERM ("Not a function.", [f]);
    1.45  
    1.46          val f_simps =
    1.47            filter (fn r =>
    1.48 @@ -121,20 +120,18 @@
    1.49          val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
    1.50          val asms_thms = map Thm.assume asms;
    1.51  
    1.52 -        fun prep_subgoal i =
    1.53 +        fun prep_subgoal_tac i =
    1.54            REPEAT (eresolve_tac @{thms Pair_inject} i)
    1.55            THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
    1.56            THEN propagate_tac i
    1.57            THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
    1.58            THEN bool_subst_tac ctxt i;
    1.59  
    1.60 -      val tac = ALLGOALS prep_subgoal;
    1.61 -
    1.62        val elim_stripped =
    1.63          nth cases idx
    1.64          |> Thm.forall_elim @{cterm "P::bool"}
    1.65          |> Thm.forall_elim (cterm_of thy args)
    1.66 -        |> Tactic.rule_by_tactic ctxt tac
    1.67 +        |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
    1.68          |> fold_rev Thm.implies_intr asms
    1.69          |> Thm.forall_intr (cterm_of thy rhs_var);
    1.70