author | traytel |
Mon, 04 Nov 2013 14:54:29 +0100 | |
changeset 54244 | 0753e8866ac8 |
parent 54243 | a596292be9a8 |
child 54245 | f91022745c85 |
--- 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'