src/HOL/Tools/coinduction.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59970 e9f73d87d904
     1.1 --- a/src/HOL/Tools/coinduction.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/coinduction.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4              |> Ctr_Sugar_Util.list_exists_free vars
     1.5              |> Term.map_abs_vars (Variable.revert_fixed ctxt)
     1.6              |> fold_rev Term.absfree (names ~~ Ts)
     1.7 -            |> Proof_Context.cterm_of ctxt;
     1.8 +            |> Thm.cterm_of ctxt;
     1.9            val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm;
    1.10            val e = length eqs;
    1.11            val p = length prems;
    1.12 @@ -88,7 +88,7 @@
    1.13              EVERY' (map (fn var =>
    1.14                resolve_tac ctxt
    1.15                  [Ctr_Sugar_Util.cterm_instantiate_pos
    1.16 -                  [NONE, SOME (Proof_Context.cterm_of ctxt var)] exI]) vars),
    1.17 +                  [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
    1.18              if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
    1.19              else
    1.20                REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'