Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
direct use of Variable.is_fixed;
authorwenzelm
Wed, 27 Apr 2011 17:20:29 +0200
changeset 42486 01b03a124b81
parent 42485 4faf82d12b19
child 42487 398d7d6bba42
direct use of Variable.is_fixed;
src/HOL/Tools/Nitpick/nitpick.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle