--- a/Quot/quotient_tacs.ML	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Feb 05 14:52:27 2010 +0100
@@ -15,6 +15,7 @@
   val lift_tac: Proof.context -> thm list -> int -> tactic
   val quotient_tac: Proof.context -> int -> tactic
   val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
+  val lifted_attr: attribute
 end;
 
 structure Quotient_Tacs: QUOTIENT_TACS =
@@ -647,4 +648,15 @@
   THEN' RANGE (map mk_tac rthms)
 end
 
+(* The attribute *)
+fun lifted_attr_pre ctxt thm =
+let
+  val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
+  val glc = Syntax.check_term ctxt gl
+in
+  (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1))
+end;
+
+val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t)
+
 end; (* structure *)