Thm.full_prop_of;

--- a/src/Pure/Isar/proof_context.ML	Mon Aug 01 19:20:45 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Aug 01 19:20:46 2005 +0200
@@ -690,7 +690,8 @@
     #> Seq.map (Drule.implies_intr_list view)
     #> Seq.map (fn rule =>
       let
-        val {thy, prop, ...} = Thm.rep_thm rule;
+        val thy = Thm.theory_of_thm rule;
+        val prop = Thm.full_prop_of rule;
         val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes);
         val tfrees = gen (Term.add_term_tfree_names (prop, []));
       in