src/HOL/Tools/function_package/termination.ML
changeset 30607 c3d1590debd8
parent 30304 d8e4cd2ac2a1
     1.1 --- a/src/HOL/Tools/function_package/termination.ML	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/termination.ML	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4  
     1.5    val REPEAT : ttac -> ttac
     1.6  
     1.7 -  val wf_union_tac : tactic
     1.8 +  val wf_union_tac : Proof.context -> tactic
     1.9  end
    1.10  
    1.11  
    1.12 @@ -276,9 +276,9 @@
    1.13  
    1.14  in
    1.15  
    1.16 -fun wf_union_tac st =
    1.17 +fun wf_union_tac ctxt st =
    1.18      let
    1.19 -      val thy = theory_of_thm st
    1.20 +      val thy = ProofContext.theory_of ctxt
    1.21        val cert = cterm_of (theory_of_thm st)
    1.22        val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
    1.23  
    1.24 @@ -303,7 +303,7 @@
    1.25            THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
    1.26                   ORELSE' ((rtac @{thm conjI})
    1.27                            THEN' (rtac @{thm refl})
    1.28 -                          THEN' (CLASET' blast_tac)))     (* Solve rest of context... not very elegant *)
    1.29 +                          THEN' (blast_tac (local_claset_of ctxt))))  (* Solve rest of context... not very elegant *)
    1.30            ) i
    1.31      in
    1.32        ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])