Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Lift.thy
changeset 1683 f78c820f67c3
parent 1681 b8a07a3c1692
child 1685 721d92623c9d 
--- a/Nominal/Lift.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Lift.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -55,18 +55,18 @@
 *}
 
 ML {*
-fun lift_thm ctxt thm =
+fun lift_thm qtys ctxt thm =
 let
   val un_raw_names = rename_vars un_raws
 in
-  rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))))
+  rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm))
 end
 *}
 
 ML {*
-fun quotient_lift_consts_export spec ctxt =
+fun quotient_lift_consts_export qtys spec ctxt =
 let
-  val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt;
+  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
   val (ts_loc, defs_loc) = split_list result;
   val morphism = ProofContext.export_morphism ctxt' ctxt;
   val ts = map (Morphism.term morphism) ts_loc
nominal2