diff -r 5c5eb939f6eb -r 0c6c67e74391 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jul 06 20:00:24 2005 +0200
+++ b/src/Pure/drule.ML	Wed Jul 06 20:00:25 2005 +0200
@@ -599,10 +599,10 @@
 val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
 
 (*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
-val eq_thm_prop = op aconv o pairself Thm.prop_of;
+val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
 
 (*Useful "distance" function for BEST_FIRST*)
-val size_of_thm = size_of_term o prop_of;
+val size_of_thm = size_of_term o Thm.full_prop_of;
 
 (*maintain lists of theorems --- preserving canonical order*)
 fun del_rules rs rules = Library.gen_rems eq_thm_prop (rules, rs);
@@ -956,13 +956,13 @@
 fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
 
 
-(* collect vars in left-to-right order *)
+(* vars in left-to-right order *)
 
 fun tvars_of_terms ts = rev (Library.foldl Term.add_tvars ([], ts));
 fun vars_of_terms ts = rev (Library.foldl Term.add_vars ([], ts));
 
-fun tvars_of thm = tvars_of_terms [prop_of thm];
-fun vars_of thm = vars_of_terms [prop_of thm];
+fun tvars_of thm = tvars_of_terms [Thm.full_prop_of thm];
+fun vars_of thm = vars_of_terms [Thm.full_prop_of thm];
 
 
 (* instantiate by left-to-right occurrence of variables *)