1.1 --- a/src/Pure/Proof/proofchecker.ML	Mon Aug 08 16:38:59 2011 +0200
     1.2 +++ b/src/Pure/Proof/proofchecker.ML	Mon Aug 08 17:23:15 2011 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4      fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
     1.5            let
     1.6              val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
     1.7 -            val {prop, ...} = rep_thm thm;
     1.8 +            val prop = Thm.prop_of thm;
     1.9              val _ =
    1.10                if is_equal prop prop' then ()
    1.11                else