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.
Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.
authorberghofe
Thu, 14 Feb 2008 01:31:30 +0100
changeset 26067 728f2c325ed6
parent 26066 19df083a2bbf
child 26068 3d2a4fd4ed77
Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.
src/HOL/Nominal/nominal_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_package.ML	Wed Feb 13 15:14:17 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Feb 14 01:31:30 2008 +0100
@@ -1644,7 +1644,7 @@
             Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
               fresh_fs @
           map (fn (((P, T), (x, U)), Q) =>
-           (Var ((P, 0), HOLogic.unitT --> Logic.varifyT T --> HOLogic.boolT),
+           (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)),
             Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
               (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
           map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
isabelle