diff -r a24e26f5488c -r f3a24012e9d8 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Wed Dec 23 13:23:33 2009 +0100 +++ b/Quot/QuotMain.thy Wed Dec 23 13:45:42 2009 +0100 @@ -11,7 +11,7 @@ ("quotient_tacs.ML") begin -locale QUOT_TYPE = +locale Quot_Type = fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" and Rep :: "'b \ ('a \ bool)"