--- a/src/HOL/Tools/Function/termination.ML Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/Function/termination.ML Sat Apr 16 16:15:37 2011 +0200
@@ -197,7 +197,7 @@
fun create ctxt chain_tac descent_tac T rel =
let
- val thy = ProofContext.theory_of ctxt
+ val thy = Proof_Context.theory_of ctxt
val sk = mk_sum_skel rel
val Ts = node_types sk T
val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
@@ -272,7 +272,7 @@
fun wf_union_tac ctxt st =
let
- val thy = ProofContext.theory_of ctxt
+ val thy = Proof_Context.theory_of ctxt
val cert = cterm_of (theory_of_thm st)
val ((_ $ (_ $ rel)) :: ineqs) = prems_of st