src/HOL/Library/refute.ML
changeset 55411 27de2c976d90
parent 54757 4960647932ec
child 55507 5f27fb2110e0
--- 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;