--- a/Nominal/Perm.thy	Fri Jul 02 15:34:46 2010 +0100
+++ b/Nominal/Perm.thy	Wed Jul 07 09:34:00 2010 +0100
@@ -24,38 +24,4 @@
 ML {* open Nominal_Dt_Quot *}
 
 
-(* permutations for quotient types *)
-
-ML {*
-fun quotient_lift_consts_export qtys spec ctxt =
-let
-  val (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt;
-  val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) result);
-  val morphism = ProofContext.export_morphism ctxt' ctxt;
-  val ts = map (Morphism.term morphism) ts_loc
-  val defs = Morphism.fact morphism defs_loc
-in
-  (ts, defs, ctxt')
 end
-*}
-
-
-
-ML {*
-fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
-let
-  val lthy =
-    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
-  val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;
-  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
-  fun tac _ =
-    Class.intro_classes_tac [] THEN
-    (ALLGOALS (resolve_tac lifted_thms))
-  val lthy'' = Class.prove_instantiation_instance tac lthy'
-in
-  Local_Theory.exit_global lthy''
-end
-*}
-
-
-end