src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
changeset 58957 c9e744ea8a38
parent 58880 0baae4311a9f
child 61999 89291b5d0ede
     1.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -297,7 +297,8 @@
     1.4  fun mkex_induct_tac ctxt sch exA exB =
     1.5    EVERY'[Seq_induct_tac ctxt sch defs,
     1.6           asm_full_simp_tac ctxt,
     1.7 -         SELECT_GOAL (safe_tac @{theory_context Fun}),
     1.8 +         SELECT_GOAL
     1.9 +          (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
    1.10           Seq_case_simp_tac ctxt exA,
    1.11           Seq_case_simp_tac ctxt exB,
    1.12           asm_full_simp_tac ctxt,