diff -r deb5be0115a7 -r 77f448727bf9 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Sat Aug 21 20:07:36 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-theory Lift
-imports "../Nominal-General/Nominal2_Atoms"
-        "../Nominal-General/Nominal2_Eqvt"
-        "../Nominal-General/Nominal2_Supp"
-        "Abs" "Perm" "Rsp"
-begin
-
-ML {*
-fun define_quotient_types binds tys alphas equivps ctxt =
-let
-  fun def_ty ((b, ty), (alpha, equivp)) ctxt =
-    Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt;
-  val alpha_equivps = List.take (equivps, length alphas)
-  val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt;
-  val qtys = map #qtyp qinfo;
-in
-  (qtys, ctxt')
-end
-*}
-
-(* Unrawifying schematic and bound variables *)
-
-ML {*
-fun unraw_str s = 
-  unsuffix "_raw" s
-  handle Fail _ => s
-
-fun unraw_vars_thm thm =
-let
-  fun unraw_var ((s, i), T) = ((unraw_str s, i), T)
-
-  val vars = Term.add_vars (prop_of thm) []
-  val nvars = map (Var o unraw_var) vars
-in
-  Thm.certify_instantiate ([], (vars ~~ nvars))  thm
-end
-*}
-
-ML {*
-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
-*}
-
-
-ML {*
-fun lift_thm qtys ctxt thm =
-  Quotient_Tacs.lifted qtys ctxt thm
-  |> unraw_bounds_thm
-  |> unraw_vars_thm
-*}
-
-
-end
-