--- 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
--- 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;