changeset 44058 | ae85c5d64913 |
parent 44057 | fda143b5c2f5 |
child 44061 | 9f17ede679e9 |
--- a/src/Pure/Proof/proofchecker.ML Mon Aug 08 16:38:59 2011 +0200 +++ b/src/Pure/Proof/proofchecker.ML Mon Aug 08 17:23:15 2011 +0200 @@ -86,7 +86,7 @@ fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) = let val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); - val {prop, ...} = rep_thm thm; + val prop = Thm.prop_of thm; val _ = if is_equal prop prop' then () else