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/BNF/Tools/bnf_fp_n2m.ML
changeset 54244 0753e8866ac8
parent 54242 99ef8036fb3d
child 54298 347c3b0cab44 
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 04 14:46:38 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 04 14:54:29 2013 +0100
@@ -121,7 +121,8 @@
               in
                 Term.list_comb (rel, rels)
               end
-          | mk_rel (T as TFree _) _ = nth phis (find_index (curry op = T) As)
+          | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
+              handle General.Subscript => HOLogic.eq_const T)
           | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
       in
         map2 (abstract oo mk_rel) fpTs fpTs'
isabelle