direct use of Variable.is_fixed;
authorwenzelm
Wed Apr 27 17:20:29 2011 +0200 (2011-04-27)
changeset 4248601b03a124b81
parent 42485 4faf82d12b19
child 42487 398d7d6bba42
direct use of Variable.is_fixed;
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 27 14:11:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 27 17:20:29 2011 +0200
     1.3 @@ -1047,15 +1047,14 @@
     1.4        end
     1.5    end
     1.6  
     1.7 -fun is_fixed_equation fixes
     1.8 +fun is_fixed_equation ctxt
     1.9                        (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
    1.10 -    member (op =) fixes s
    1.11 +    Variable.is_fixed ctxt s
    1.12    | is_fixed_equation _ _ = false
    1.13  fun extract_fixed_frees ctxt (assms, t) =
    1.14    let
    1.15 -    val fixes = Variable.fixes_of ctxt |> map snd
    1.16      val (subst, other_assms) =
    1.17 -      List.partition (is_fixed_equation fixes) assms
    1.18 +      List.partition (is_fixed_equation ctxt) assms
    1.19        |>> map Logic.dest_equals
    1.20    in (subst, other_assms, subst_atomic subst t) end
    1.21