diff -r 741978011e12 -r d65f461c8672 src/Pure/IsaPlanner/term_lib.ML
--- a/src/Pure/IsaPlanner/term_lib.ML	Fri Apr 22 14:15:01 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Fri Apr 22 15:10:42 2005 +0200
@@ -63,6 +63,7 @@
     val try_dest_Trueprop : Term.term -> Term.term
 
     val bot_left_leaf_of : Term.term -> Term.term
+    val bot_left_leaf_noabs_of : Term.term -> Term.term
 
     (* term containing another term - an embedding check *)
     val term_contains : Term.term -> Term.term -> bool
@@ -93,6 +94,10 @@
     (* get the frees in a term that are of atomic type, ie non-functions *)
     val atomic_frees_of_term : Term.term -> (string * Term.typ) list
 
+    (* get used names in a theorem to avoid upon instantiation. *)
+    val usednames_of_term : Term.term -> string list
+    val usednames_of_thm : Thm.thm -> string list
+
     (* Isar term skolemisationm and unsolemisation *)
     (* I think this is written also in IsarRTechn and also in somewhere else *)
     (* val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term
@@ -113,9 +118,11 @@
     val pretty_print_typelist :
        Term.typ list -> (Term.typ -> string) -> string
  
+    (* for debugging: quickly get a string of a term w.r.t the_context() *)
     val string_of_term : Term.term -> string
 
-    (* these are perhaps redundent, check the standard basis 
+    (* Pretty printing in a way that allows them to be parsed by ML.
+       these are perhaps redundent, check the standard basis 
        lib for generic versions for any datatype? *)
     val writesort : string list -> unit
     val writeterm : Term.term -> unit
@@ -387,6 +394,15 @@
      o map Term.dest_Free 
      o Term.term_frees;
 
+fun usednames_of_term t = Term.add_term_names (t,[]);
+fun usednames_of_thm th = 
+    let val rep = Thm.rep_thm th
+      val hyps = #hyps rep
+      val (tpairl,tpairr) = Library.split_list (#tpairs rep)
+      val prop = #prop rep 
+    in
+      List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
+    end;
 
 (* read in a string and a top-level type and this will give back a term *) 
 fun readwty tstr tystr = 
@@ -460,11 +476,12 @@
 (* FIXME: we should really check that there is a subterm on the lhs
 which embeds into the rhs, this would be much closer to the normal
 notion of valid wave rule - ie there exists at least one case where it
-is a valid wave rule... *)                                        
+is a valid wave rule... *)
 	fun is_not_valid_rwrule tysig (lhs, rhs) = 
-			(Pattern.matches_subterm tysig (lhs, rhs)) orelse
-			has_new_vars (lhs,rhs) orelse
-      has_new_typ_vars (lhs,rhs);
+      Term.is_Var (Term.head_of lhs) (* if lhs is essentially just a var *)
+      orelse has_new_vars (lhs,rhs) 
+      orelse has_new_typ_vars (lhs,rhs) 
+      orelse Pattern.matches_subterm tysig (lhs, rhs);
 
 
   (* first term contains the second in some name convertable way... *)
@@ -739,6 +756,8 @@
     | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
     | bot_left_leaf_of x = x;
 
+  fun bot_left_leaf_noabs_of (l $ r) = bot_left_leaf_noabs_of l
+    | bot_left_leaf_noabs_of x = x;
 
 (* cleaned up normal form version of the subgoal terms conclusion *)
 fun cleaned_term_conc t =