# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 27de2c976d904ee652667c97ef29805101bc0ff1
# Parent  54b09e82b9e1f8841aeb641e66432fd7a3fc0f74
repaired hard-coded constant names

diff -r 54b09e82b9e1 -r 27de2c976d90 src/HOL/Library/refute.ML
--- 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;
diff -r 54b09e82b9e1 -r 27de2c976d90 src/HOL/Tools/TFL/rules.ML
--- 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 =
diff -r 54b09e82b9e1 -r 27de2c976d90 src/HOL/Tools/hologic.ML
--- 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) =