diff -r a908ea36054f -r 4c5881455923 Nominal/Perm.thy --- 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