src/HOL/Tools/Function/termination.ML
changeset 59621 291934bac95e
parent 59618 e6939796717e
child 59625 aacdce52b2fc
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4          Const (@{const_abbrev Set.empty}, fastype_of c1))
     1.5        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
     1.6    in
     1.7 -    case Function_Lib.try_proof (Proof_Context.cterm_of ctxt goal) chain_tac of
     1.8 +    case Function_Lib.try_proof (Thm.cterm_of ctxt goal) chain_tac of
     1.9        Function_Lib.Solved thm => SOME thm
    1.10      | _ => NONE
    1.11    end
    1.12 @@ -169,7 +169,7 @@
    1.13  fun mk_desc ctxt tac vs Gam l r m1 m2 =
    1.14    let
    1.15      fun try rel =
    1.16 -      try_proof (Proof_Context.cterm_of ctxt
    1.17 +      try_proof (Thm.cterm_of ctxt
    1.18          (Logic.list_all (vs,
    1.19             Logic.mk_implies (HOLogic.mk_Trueprop Gam,
    1.20               HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
    1.21 @@ -302,7 +302,7 @@
    1.22            THEN' (blast_tac ctxt)))    (* Solve rest of context... not very elegant *)
    1.23        ) i
    1.24    in
    1.25 -    (PRIMITIVE (Drule.cterm_instantiate [apply2 (Proof_Context.cterm_of ctxt) (rel, relation)])
    1.26 +    (PRIMITIVE (Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
    1.27       THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
    1.28       THEN rewrite_goal_tac ctxt Un_aci_simps 1)  (* eliminate duplicates *)
    1.29    end) 1 st