--- a/Nominal/nominal_dt_quot.ML	Sat Aug 21 17:55:42 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sat Aug 21 20:07:36 2010 +0800
@@ -2,7 +2,7 @@
     Author:     Christian Urban
     Author:     Cezary Kaliszyk
 
-  Performing quotient constructions
+  Performing quotient constructions and lifting theorems
 *)
 
 signature NOMINAL_DT_QUOT =
@@ -18,6 +18,8 @@
 
   val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> 
     local_theory -> local_theory
+
+  val lift_thm: typ list -> Proof.context -> thm -> thm
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -79,5 +81,36 @@
   |> Named_Target.theory_init
 end
 
+
+(* lifts a theorem and deletes all "_raw" suffixes *)
+
+fun unraw_str s = 
+  unsuffix "_raw" s
+  handle Fail _ => s
+
+fun unraw_vars_thm thm =
+let
+  fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
+
+  val vars = Term.add_vars (prop_of thm) []
+  val vars' = map (Var o unraw_var_str) vars
+in
+  Thm.certify_instantiate ([], (vars ~~ vars')) thm
+end
+
+fun unraw_bounds_thm th =
+let
+  val trm = Thm.prop_of th
+  val trm' = Term.map_abs_vars unraw_str trm
+in
+  Thm.rename_boundvars trm trm' th
+end
+
+fun lift_thm qtys ctxt thm =
+  Quotient_Tacs.lifted qtys ctxt thm
+  |> unraw_bounds_thm
+  |> unraw_vars_thm
+
+
 end (* structure *)