src/HOL/Library/rewrite.ML
changeset 59970 e9f73d87d904
parent 59739 4ed50ebf5d36
child 59975 da10875adf8e
     1.1 --- a/src/HOL/Library/rewrite.ML	Wed Apr 08 16:24:22 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Wed Apr 08 19:39:08 2015 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4    | _ => raise TERM ("ft_assm", [t])
     1.5  
     1.6  fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
     1.7 -  if Object_Logic.is_judgment (Proof_Context.theory_of ctxt) t
     1.8 +  if Object_Logic.is_judgment ctxt t
     1.9    then ft_arg ctxt ft
    1.10    else ft
    1.11