src/HOL/HOLCF/Tools/Domain/domain_induction.ML
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 54895 515630483010
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -161,12 +161,12 @@
     1.4                val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules)
     1.5                fun arg_tac (lazy, _) =
     1.6                    rtac (if lazy then allI else case_UU_allI) 1
     1.7 -              val tacs =
     1.8 -                  rewrite_goals_tac @{thms atomize_all atomize_imp} ::
     1.9 +              fun tacs ctxt =
    1.10 +                  rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} ::
    1.11                    map arg_tac args @
    1.12                    [REPEAT (rtac impI 1), ALLGOALS simplify]
    1.13              in
    1.14 -              Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
    1.15 +              Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context)
    1.16              end
    1.17            fun eq_thms (p, cons) = map (con_thm p) cons
    1.18            val conss = map #con_specs constr_infos
    1.19 @@ -321,7 +321,7 @@
    1.20        val rules = @{thm Rep_cfun_strict1} :: take_0_thms
    1.21        fun tacf {prems, context = ctxt} =
    1.22          let
    1.23 -          val prem' = rewrite_rule [bisim_def_thm] (hd prems)
    1.24 +          val prem' = rewrite_rule ctxt [bisim_def_thm] (hd prems)
    1.25            val prems' = Project_Rule.projections ctxt prem'
    1.26            val dests = map (fn th => th RS spec RS spec RS mp) prems'
    1.27            fun one_tac (dest, rews) =