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.
tuned;
authorwenzelm
Mon, 12 Sep 2016 20:31:28 +0200
changeset 63858 0f5e735e3640
parent 63857 0883c1cc655c
child 63859 dca6fabd8060
tuned;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/thm.ML	Mon Sep 12 20:24:42 2016 +0200
+++ b/src/Pure/thm.ML	Mon Sep 12 20:31:28 2016 +0200
@@ -1410,7 +1410,7 @@
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
       Thm (deriv_rule1
-          ((if Envir.is_empty env then I else (Proofterm.norm_proof' env)) o
+          ((if Envir.is_empty env then I else Proofterm.norm_proof' env) o
             Proofterm.assumption_proof Bs Bi n) der,
        {tags = [],
         maxidx = Envir.maxidx_of env,
isabelle