Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/coherent.ML
changeset 42488 4638622bcaa1
parent 42361 23f352990944
child 46186 9ae331a1d8c5 
--- a/src/Tools/coherent.ML	Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Tools/coherent.ML	Wed Apr 27 17:58:45 2011 +0200
@@ -213,7 +213,7 @@
   SUBPROOF (fn {prems = prems', concl, context, ...} =>
     let val xs = map (term_of o #2) params @
       map (fn (_, s) => Free (s, the (Variable.default_type context s)))
-        (Variable.fixes_of context)
+        (rev (Variable.dest_fixes context))  (* FIXME !? *)
     in
       case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
            (mk_dom xs) Net.empty 0 0 of
isabelle