tuned;
authorwenzelm
Thu Apr 10 10:36:29 2014 +0200 (2014-04-10)
changeset 56506c1f04411d43f
parent 56505 aed94b61f65b
child 56507 5f6f2576a836
tuned;
src/HOL/Tools/cnf.ML
src/Tools/induction.ML
     1.1 --- a/src/HOL/Tools/cnf.ML	Thu Apr 10 10:30:32 2014 +0200
     1.2 +++ b/src/HOL/Tools/cnf.ML	Thu Apr 10 10:36:29 2014 +0200
     1.3 @@ -207,9 +207,9 @@
     1.4        in
     1.5          make_nnf_iff OF [thm1, thm2, thm3, thm4]
     1.6        end
     1.7 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
     1.8 +  | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
     1.9        make_nnf_not_false
    1.10 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
    1.11 +  | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
    1.12        make_nnf_not_true
    1.13    | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
    1.14        let
     2.1 --- a/src/Tools/induction.ML	Thu Apr 10 10:30:32 2014 +0200
     2.2 +++ b/src/Tools/induction.ML	Thu Apr 10 10:36:29 2014 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4    | (p as Free _, _) => [p]
     2.5    | (_, ts) => flat(map preds_of ts))
     2.6  
     2.7 -fun name_hyps thy (arg as ((cases,consumes),th)) =
     2.8 +fun name_hyps (arg as ((cases, consumes), th)) =
     2.9    if not(forall (null o #2 o #1) cases) then arg
    2.10    else
    2.11      let
    2.12 @@ -35,7 +35,7 @@
    2.13          (take n cases ~~ take n hnamess)
    2.14      in ((cases',consumes),th) end
    2.15  
    2.16 -val induction_tac = Induct.gen_induct_tac name_hyps
    2.17 +val induction_tac = Induct.gen_induct_tac (K name_hyps)
    2.18  
    2.19  val setup = Induct.gen_induct_setup @{binding induction} induction_tac
    2.20