--- a/src/HOL/Quotient.thy Fri Mar 23 16:16:35 2012 +0000 +++ b/src/HOL/Quotient.thy Fri Mar 23 18:23:47 2012 +0100 @@ -960,4 +960,6 @@ map_fun (infixr "--->" 55) and fun_rel (infixr "===>" 55) +hide_const (open) invariant + end