# HG changeset patch
# User wenzelm
# Date 1413276766 -7200
# Node ID 6bade3d91c496b3793bd2f3c5fe5ae4171ac8e1b
# Parent  1891f17c612470dd91f9305ed9c00e836c3c209a
tuned signature;

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 
diff -r 1891f17c6124 -r 6bade3d91c49 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Oct 13 22:43:29 2014 +0200
+++ b/src/Pure/theory.ML	Tue Oct 14 10:52:46 2014 +0200
@@ -8,7 +8,6 @@
 sig
   val eq_thy: theory * theory -> bool
   val subthy: theory * theory -> bool
-  val assert_super: theory -> theory -> theory
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val nodes_of: theory -> theory list
@@ -43,10 +42,6 @@
 val eq_thy = Context.eq_thy;
 val subthy = Context.subthy;
 
-fun assert_super thy1 thy2 =
-  if subthy (thy1, thy2) then thy2
-  else raise THEORY ("Not a super theory", [thy1, thy2]);
-
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;
 fun nodes_of thy = thy :: ancestors_of thy;