diff -r 1891f17c6124 -r 6bade3d91c49 src/HOL/Matrix_LP/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Mon Oct 13 22:43:29 2014 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Oct 14 10:52:46 2014 +0200
@@ -187,6 +187,11 @@
 
 fun ref_of (Computer r) = r
 
+fun super_theory thy1 thy2 =
+  if Theory.subthy (thy1, thy2) then thy2
+  else raise THEORY ("Not a super theory", [thy1, thy2]);
+
+
 datatype cthm = ComputeThm of term list * sort list * term
 
 fun thm2cthm th = 
@@ -374,7 +379,7 @@
     let
         val thy = Thm.theory_of_cterm ct
         val {t=t',T=ty,...} = rep_cterm ct
-        val _ = Theory.assert_super (theory_of computer) thy
+        val _ = super_theory (theory_of computer) thy
         val naming = naming_of computer
         val (encoding, t) = remove_types (encoding_of computer) t'
         val t = runprog (prog_of computer) t
@@ -396,7 +401,7 @@
 
 fun make_theorem computer th vars =
 let
-    val _ = Theory.assert_super (theory_of computer) (theory_of_thm th)
+    val _ = super_theory (theory_of computer) (theory_of_thm th)
 
     val (ComputeThm (hyps, shyps, prop)) = thm2cthm th 
 
@@ -501,7 +506,7 @@
 
     fun compute_inst (s, ct) vs =
         let
-            val _ = Theory.assert_super (theory_of_cterm ct) thy
+            val _ = super_theory (theory_of_cterm ct) thy
             val ty = typ_of (ctyp_of_term ct) 
         in          
             (case Symtab.lookup vartab s of