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.
Added missing "standard"
authornipkow
Fri, 01 Dec 2006 16:08:45 +0100
changeset 21618 1cbb1134cb6c
parent 21617 4664489469fc
child 21619 dea0914773f7
Added missing "standard"
src/HOL/Nominal/nominal_primrec.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 01 12:23:53 2006 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 01 16:08:45 2006 +0100
@@ -354,7 +354,7 @@
     Proof.theorem_i NONE
       (fn thss => ProofContext.theory (fn thy =>
          let
-           val simps = flat thss;
+           val simps = map standard (flat thss);
            val (simps', thy') =
              fold_map note ((map fst eqns ~~ atts) ~~ map single simps) thy;
            val simps'' = maps snd simps'
isabelle