--- a/src/HOL/Library/refute.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/refute.ML Wed Feb 12 08:35:56 2014 +0100
@@ -3163,8 +3163,8 @@
add_interpreter "lfp" lfp_interpreter #>
add_interpreter "gfp" gfp_interpreter #>
*)
- add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #>
- add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #>
+ add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
+ add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
add_printer "stlc" stlc_printer #>
add_printer "set" set_printer #>
add_printer "IDT" IDT_printer;
--- 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 =
--- a/src/HOL/Tools/hologic.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/hologic.ML Wed Feb 12 08:35:56 2014 +0100
@@ -348,12 +348,12 @@
fun mk_fst p =
let val pT = fastype_of p in
- Const ("Product_Type.fst", pT --> fst (dest_prodT pT)) $ p
+ Const ("Product_Type.prod.fst", pT --> fst (dest_prodT pT)) $ p
end;
fun mk_snd p =
let val pT = fastype_of p in
- Const ("Product_Type.snd", pT --> snd (dest_prodT pT)) $ p
+ Const ("Product_Type.prod.snd", pT --> snd (dest_prodT pT)) $ p
end;
fun split_const (A, B, C) =