--- a/Nominal/Lift.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Lift.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -3,6 +3,18 @@
 begin
 
 ML {*
+fun define_quotient_type args tac ctxt =
+let
+  val mthd = Method.SIMPLE_METHOD tac
+  val mthdt = Method.Basic (fn _ => mthd)
+  val bymt = Proof.global_terminal_proof (mthdt, NONE)
+in
+  bymt (Quotient_Type.quotient_type args ctxt)
+end
+*}
+
+(* Renames schematic variables in a theorem *)
+ML {*
 fun rename_vars fnctn thm =
 let
   val vars = Term.add_vars (prop_of thm) []