src/Pure/Proof/proofchecker.ML

--- a/src/Pure/Proof/proofchecker.ML	Sat Nov 15 21:31:30 2008 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Sat Nov 15 21:31:32 2008 +0100
@@ -45,7 +45,7 @@
         Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
       end;
 
-    fun thm_of _ _ (PThm (name, _, prop', SOME Ts)) =
+    fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
           let
             val thm = Drule.implies_intr_hyps (lookup name);
             val {prop, ...} = rep_thm thm;