src/HOL/Tools/coinduction.ML
changeset 59970 e9f73d87d904
parent 59621 291934bac95e
child 59971 ea06500bb092
     1.1 --- a/src/HOL/Tools/coinduction.ML	Wed Apr 08 16:24:22 2015 +0200
     1.2 +++ b/src/HOL/Tools/coinduction.ML	Wed Apr 08 19:39:08 2015 +0200
     1.3 @@ -98,9 +98,9 @@
     1.4                 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
     1.5                   (case prems of
     1.6                     [] => all_tac
     1.7 -                 | inv::case_prems =>
     1.8 +                 | inv :: case_prems =>
     1.9                       let
    1.10 -                       val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
    1.11 +                       val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
    1.12                         val inv_thms = init @ [last];
    1.13                         val eqs = take e inv_thms;
    1.14                         fun is_local_var t =
    1.15 @@ -115,7 +115,7 @@
    1.16          end) ctxt) THEN'
    1.17        K (prune_params_tac ctxt))
    1.18      #> Seq.maps (fn st =>
    1.19 -      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of st) cases) all_tac st)
    1.20 +      CASES (Rule_Cases.make_common ctxt (Thm.prop_of st) cases) all_tac st)
    1.21    end));
    1.22  
    1.23  local