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/Perm.thy
changeset 2335 558c823f96aa
parent 2305 93ab397f5980
child 2337 b151399bd2c3 
--- a/Nominal/Perm.thy	Thu Jun 24 00:41:41 2010 +0100
+++ b/Nominal/Perm.thy	Thu Jun 24 19:32:33 2010 +0100
@@ -24,8 +24,8 @@
 ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
 let
-  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
-  val (ts_loc, defs_loc) = split_list result;
+  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
nominal2