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.
Drule.implies_intr_hyps;
authorwenzelm
Wed, 29 Jun 2005 15:13:38 +0200
changeset 16608 4f8d7b83c7e2
parent 16607 81e687c63e29
child 16609 c787112bba1f
Drule.implies_intr_hyps;
src/Pure/Proof/proofchecker.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Proof/proofchecker.ML	Wed Jun 29 15:13:37 2005 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Wed Jun 29 15:13:38 2005 +0200
@@ -47,7 +47,7 @@
 
     fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) =
           let
-            val thm = Thm.implies_intr_hyps (lookup name);
+            val thm = Drule.implies_intr_hyps (lookup name);
             val {prop, ...} = rep_thm thm;
             val _ = if prop aconv prop' then () else
               error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
isabelle