Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Theory.subthy;
authorwenzelm
Tue, 15 Apr 2008 18:49:29 +0200
changeset 26674 fe93963ed76d
parent 26673 cda3df424bad
child 26675 fba93ce71435
Theory.subthy;
src/Tools/Compute_Oracle/compute.ML file | annotate | diff | comparison | revisions 
--- a/src/Tools/Compute_Oracle/compute.ML	Tue Apr 15 18:49:28 2008 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Tue Apr 15 18:49:29 2008 +0200
@@ -640,8 +640,8 @@
             val thy1 = theory_of_theorem th
             val thy2 = theory_of_thm th'
         in
-            if Context.subthy (thy1, thy2) then thy2 
-            else if Context.subthy (thy2, thy1) then thy1 else
+            if Theory.subthy (thy1, thy2) then thy2 
+            else if Theory.subthy (thy2, thy1) then thy1 else
             raise Compute "modus_ponens: theorems are not compatible with each other"
         end 
     val th' = make_theorem computer th' []
isabelle