src/Pure/Thy/term_style.ML
changeset 35625 9c818cab0dd0
parent 33522 737589bb9bb8
child 36950 75b8f26f2f07
--- 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)