diff -r 41f89d4f9548 -r 4a4c714ff795 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Wed Feb 10 17:10:52 2010 +0100 +++ b/Quot/QuotMain.thy Wed Feb 10 17:22:18 2010 +0100 @@ -12,7 +12,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)"