--- a/QuotMain.thy	Tue Nov 03 18:09:59 2009 +0100
+++ b/QuotMain.thy	Wed Nov 04 09:52:31 2009 +0100
@@ -1058,6 +1058,16 @@
 end
 *}
 
+ML {*
+  fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
+    let
+      val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
+      val (_, lthy2) = note (name, lifted_thm) lthy;
+    in
+      lthy2
+    end;
+*}
+
 
 end