--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Feb 25 22:32:09 2010 +0100
@@ -70,7 +70,7 @@
val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
- foldr1 (HOLogic.mk_binop "op &")
+ foldr1 (HOLogic.mk_binop @{const_name "op &"})
(map HOLogic.mk_eq (frees ~~ frees')))))
end;
in
@@ -149,7 +149,7 @@
val prems = maps (fn ((i, (_, _, constrs)), T) =>
map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = make_tnames recTs;
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
(descr' ~~ recTs ~~ tnames)))