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.
QuotMain.thy
changeset 540 c0b13fb70d6d
parent 539 8287fb5b8d7a
child 541 94deffed619d 
--- a/QuotMain.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -1081,7 +1081,7 @@
     val thy = ProofContext.theory_of lthy;
     val quotients = quotient_rules_get lthy
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-    val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients
+    val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
     val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
nominal2