--- a/QuotMain.thy	Thu Dec 03 11:34:34 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 11:40:10 2009 +0100
@@ -716,6 +716,7 @@
 section {* RepAbs Injection Tactic *}
 
 (* TODO: check if it still works with first_order_match *)
+(* FIXME/TODO: do not handle everything *)x
 ML {*
 fun instantiate_tac thm = 
   Subgoal.FOCUS (fn {concl, ...} =>
@@ -771,14 +772,6 @@
       | _ => no_tac)
 *}
 
-ML {* (* Legacy *)
-fun needs_lift (rty as Type (rty_s, _)) ty =
-  case ty of
-    Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys)
-  | _ => false
-
-*}
-
 definition
   "QUOT_TRUE x \<equiv> True"