# HG changeset patch
# User wenzelm
# Date 1303917629 -7200
# Node ID 01b03a124b81d11e98b9445a419add54d7e88fdc
# Parent  4faf82d12b194b961f9ee1c681549e04b2ca78a2
direct use of Variable.is_fixed;

diff -r 4faf82d12b19 -r 01b03a124b81 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 27 14:11:37 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 27 17:20:29 2011 +0200
@@ -1047,15 +1047,14 @@
       end
   end
 
-fun is_fixed_equation fixes
+fun is_fixed_equation ctxt
                       (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
-    member (op =) fixes s
+    Variable.is_fixed ctxt s
   | is_fixed_equation _ _ = false
 fun extract_fixed_frees ctxt (assms, t) =
   let
-    val fixes = Variable.fixes_of ctxt |> map snd
     val (subst, other_assms) =
-      List.partition (is_fixed_equation fixes) assms
+      List.partition (is_fixed_equation ctxt) assms
       |>> map Logic.dest_equals
   in (subst, other_assms, subst_atomic subst t) end