# HG changeset patch
# User wenzelm
# Date 1122916846 -7200
# Node ID 38bb4f03a8877ec0397c5ac84ffaa8fbfa0ee81a
# Parent  39f5760f72d77f670646e47599703a342bbff040
Thm.full_prop_of;

diff -r 39f5760f72d7 -r 38bb4f03a887 src/Pure/Isar/proof_context.ML
--- 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