src/HOL/Tools/Function/induction_schema.ML
changeset 51717 9e7d1c139569
parent 47432 e1576d13e933
child 52223 5bb6ae8acb87
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -231,7 +231,7 @@
     1.4      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
     1.5      val pats = map_index (uncurry inject) xss
     1.6      val sum_split_rule =
     1.7 -      Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
     1.8 +      Pat_Completeness.prove_completeness ctxt [x] (P_comp $ x) xss (map single pats)
     1.9  
    1.10      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
    1.11        let
    1.12 @@ -253,8 +253,9 @@
    1.13              val cqs = map (cert o Free) qs
    1.14              val ags = map (Thm.assume o cert) gs
    1.15  
    1.16 -            val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
    1.17 -            val sih = full_simplify replace_x_ss aihyp
    1.18 +            val replace_x_simpset =
    1.19 +              put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps)
    1.20 +            val sih = full_simplify replace_x_simpset aihyp
    1.21  
    1.22              fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
    1.23                let
    1.24 @@ -373,7 +374,7 @@
    1.25        in
    1.26          indthm
    1.27          |> Drule.instantiate' [] [SOME inst]
    1.28 -        |> simplify SumTree.sumcase_split_ss
    1.29 +        |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
    1.30          |> Conv.fconv_rule ind_rulify
    1.31        end
    1.32