src/HOL/Tools/res_clause.ML
changeset 21254 d53f76357f41
parent 20854 f9cf9e62d11c
child 21290 33b6bb5d6ab8
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Nov 08 21:45:14 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Nov 08 21:45:15 2006 +0100
     1.3 @@ -125,15 +125,15 @@
     1.4  		   ("op Un", "union"),
     1.5  		   ("op Int", "inter"),
     1.6  		   ("List.op @", "append"),
     1.7 -		   ("Reconstruction.fequal", "fequal"),
     1.8 -		   ("Reconstruction.COMBI", "COMBI"),
     1.9 -		   ("Reconstruction.COMBK", "COMBK"),
    1.10 -		   ("Reconstruction.COMBB", "COMBB"),
    1.11 -		   ("Reconstruction.COMBC", "COMBC"),
    1.12 -		   ("Reconstruction.COMBS", "COMBS"),
    1.13 -		   ("Reconstruction.COMBB'", "COMBB_e"),
    1.14 -		   ("Reconstruction.COMBC'", "COMBC_e"),
    1.15 -		   ("Reconstruction.COMBS'", "COMBS_e")];
    1.16 +		   ("ATP_Linkup.fequal", "fequal"),
    1.17 +		   ("ATP_Linkup.COMBI", "COMBI"),
    1.18 +		   ("ATP_Linkup.COMBK", "COMBK"),
    1.19 +		   ("ATP_Linkup.COMBB", "COMBB"),
    1.20 +		   ("ATP_Linkup.COMBC", "COMBC"),
    1.21 +		   ("ATP_Linkup.COMBS", "COMBS"),
    1.22 +		   ("ATP_Linkup.COMBB'", "COMBB_e"),
    1.23 +		   ("ATP_Linkup.COMBC'", "COMBC_e"),
    1.24 +		   ("ATP_Linkup.COMBS'", "COMBS_e")];
    1.25  
    1.26  val type_const_trans_table =
    1.27        Symtab.make [("*", "prod"),