--- a/src/HOL/Tools/TFL/rules.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Wed Feb 12 08:35:56 2014 +0100
@@ -578,10 +578,10 @@
local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
fun mk_fst tm =
let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
- in Const ("Product_Type.fst", ty --> fty) $ tm end
+ in Const (@{const_name Product_Type.fst}, ty --> fty) $ tm end
fun mk_snd tm =
let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
- in Const ("Product_Type.snd", ty --> sty) $ tm end
+ in Const (@{const_name Product_Type.snd}, ty --> sty) $ tm end
in
fun XFILL tych x vstruct =
let fun traverse p xocc L =