--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sun Aug 16 18:19:30 2015 +0200
@@ -607,7 +607,7 @@
val thy = theory_of computer
val _ = check_compatible computer th
val _ =
- Theory.subthy (theory_of_theorem th, thy) orelse raise Compute "modus_ponens: bad theory"
+ Context.subthy (theory_of_theorem th, thy) orelse raise Compute "modus_ponens: bad theory"
val th' = make_theorem computer (Thm.transfer thy raw_th') []
val varsubst = varsubst_of_theorem th
fun run vars_allowed t =