--- 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