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.
Quot/quotient_term.ML
changeset 786 d6407afb913c
parent 785 bf6861ee3b90
child 790 3a48ffcf0f9a 
--- a/Quot/quotient_term.ML	Wed Dec 23 23:53:03 2009 +0100
+++ b/Quot/quotient_term.ML	Thu Dec 24 00:58:50 2009 +0100
@@ -154,7 +154,7 @@
        else 
          let
            val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") 
-           val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc
+           val equiv_rel = #equiv_rel (quotdata_lookup thy s') handle NotFound => raise exc
            (* FIXME: check in this case that the rty and qty *)
            (* FIXME: correspond to each other *)
nominal2