src/Pure/Thy/term_style.ML
changeset 35625 9c818cab0dd0
parent 33522 737589bb9bb8
child 36950 75b8f26f2f07
     1.1 --- a/src/Pure/Thy/term_style.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Thy/term_style.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -64,8 +64,8 @@
     1.4  
     1.5  fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
     1.6    let
     1.7 -    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
     1.8 -      (Logic.strip_imp_concl t)
     1.9 +    val concl =
    1.10 +      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
    1.11    in
    1.12      case concl of (_ $ l $ r) => proj (l, r)
    1.13      | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)