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/HOL/Tools/SMT2/z3_new_isar.ML
changeset 57748 31f5781fa9cd
parent 57745 c65c116553b5
child 57749 ce40cee07fbc 
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -72,7 +72,7 @@
       let
         val sid = string_of_int id
 
-        val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
+        val concl' = postprocess_step_conclusion thy rewrite_rules ll_defs concl
         fun standard_step role =
           ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
            map (fn id => (string_of_int id, [])) prems)
isabelle