# HG changeset patch
# User wenzelm
# Date 1120050818 -7200
# Node ID 4f8d7b83c7e2559b323b0e972225d4cea1863205
# Parent  81e687c63e2941441512a7d5b7cd9ba09b4461f8
Drule.implies_intr_hyps;

diff -r 81e687c63e29 -r 4f8d7b83c7e2 src/Pure/Proof/proofchecker.ML
--- 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" ^