diff -r 62e1d888aacc -r 60c4c93b30d5 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jan 24 14:05:24 2012 +0000
+++ b/Quotient-Paper/Paper.thy	Tue Jan 24 14:29:07 2012 +0000
@@ -45,7 +45,7 @@
 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
   let
     val concl =
-      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+      Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
   in
     case concl of (_ $ l $ r) => proj (l, r)
     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)