src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 35827 f552152d7747
parent 35826 1590abc3d42a
child 35865 2f8fb5242799
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Mar 17 19:26:05 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Mar 17 19:37:44 2010 +0100
     1.3 @@ -104,15 +104,15 @@
     1.4                     (@{const_name "op |"}, "or"),
     1.5                     (@{const_name "op -->"}, "implies"),
     1.6                     (@{const_name "op :"}, "in"),
     1.7 -                   ("ATP_Linkup.fequal", "fequal"),
     1.8 -                   ("ATP_Linkup.COMBI", "COMBI"),
     1.9 -                   ("ATP_Linkup.COMBK", "COMBK"),
    1.10 -                   ("ATP_Linkup.COMBB", "COMBB"),
    1.11 -                   ("ATP_Linkup.COMBC", "COMBC"),
    1.12 -                   ("ATP_Linkup.COMBS", "COMBS"),
    1.13 -                   ("ATP_Linkup.COMBB'", "COMBB_e"),
    1.14 -                   ("ATP_Linkup.COMBC'", "COMBC_e"),
    1.15 -                   ("ATP_Linkup.COMBS'", "COMBS_e")];
    1.16 +                   ("Sledgehammer.fequal", "fequal"),
    1.17 +                   ("Sledgehammer.COMBI", "COMBI"),
    1.18 +                   ("Sledgehammer.COMBK", "COMBK"),
    1.19 +                   ("Sledgehammer.COMBB", "COMBB"),
    1.20 +                   ("Sledgehammer.COMBC", "COMBC"),
    1.21 +                   ("Sledgehammer.COMBS", "COMBS"),
    1.22 +                   ("Sledgehammer.COMBB'", "COMBB_e"),
    1.23 +                   ("Sledgehammer.COMBC'", "COMBC_e"),
    1.24 +                   ("Sledgehammer.COMBS'", "COMBS_e")];
    1.25  
    1.26  val type_const_trans_table =
    1.27        Symtab.make [("*", "prod"),