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/Pure/thm.ML
changeset 63858 0f5e735e3640
parent 63611 fb63942e470e
child 64568 a504a3dec35a 
--- 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