--- a/src/Pure/Thy/term_style.ML Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Thy/term_style.ML Sun Mar 07 12:19:47 2010 +0100
@@ -64,8 +64,8 @@
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
let
- val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
- (Logic.strip_imp_concl t)
+ val concl =
+ Object_Logic.drop_judgment (ProofContext.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)