# HG changeset patch
# User paulson
# Date 1158852670 -7200
# Node ID 8606ddd42554810da64c7e714238af36c8dcbde8
# Parent  66b8455090b8f0ff297b2aeb64531d43ae171c16
corrected for the translation from _ to __ in c_COMBx_e

diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/const_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/const_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,10 +4,10 @@
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
 a6 ).
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
 a7 ).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/const_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/const_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -4,10 +4,10 @@
 
 %B' c f g x -->  c (f (g x))
 input_clause(a6,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
 
 %C' c f g x --> c (f x) g
 input_clause(a7,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
 
 
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/const_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/const_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,5 +4,5 @@
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
 a8 ).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/const_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/const_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -4,4 +4,4 @@
 
 %S' c f g x --> c (f x) (g x)
 input_clause(a8,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/full_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/full_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,10 +4,10 @@
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB_e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B)))),
+or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB__e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B)))),
 a6 ).
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U)))),
+or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U)))),
 a7 ).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/full_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/full_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -4,9 +4,9 @@
 
 %B' c f g x -->  c (f (g x))
 input_clause(a6,axiom,
-[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB_e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B))]).
+[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB__e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B))]).
 
 
 %C' c f g x --> c (f x) g
 input_clause(a7,axiom,
-[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U))]).
+[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U))]).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/full_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/full_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,6 +4,6 @@
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U)))),
+or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U)))),
 a8 ).
 
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/full_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/full_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -5,4 +5,4 @@
 
 %S' c f g x --> c (f x) (g x)
 input_clause(a8,axiom,
-[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U))]).
+[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U))]).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/par_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/par_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,10 +4,10 @@
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B))))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B))))),
 a6 ).
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U))))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U))))),
 a7 ).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/par_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/par_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -4,8 +4,8 @@
 
 %B' c f g x -->  c (f (g x))
 input_clause(a6,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B)))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B)))]).
 
 %C' c f g x --> c (f x) g
 input_clause(a7,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U)))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U)))]).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/par_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/par_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,5 +4,5 @@
 
 clause(
 forall([A, B, C, F, G, U, V, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U))))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U))))),
 a8 ).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/par_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/par_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -4,5 +4,5 @@
 
 %S' c f g x --> c (f x) (g x)
 input_clause(a8,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U)))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U)))]).
 
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/u_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/u_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,10 +4,10 @@
 
 clause(
 forall([C, F, G, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
 a6 ).
 
 clause(
 forall([C, F, G, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
 a7 ).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/u_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/u_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -4,8 +4,8 @@
 
 %B' c f g x -->  c (f (g x))
 input_clause(a6,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
 
 %C' c f g x --> c (f x) g
 input_clause(a7,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/u_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/u_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
@@ -4,5 +4,5 @@
 
 clause(
 forall([C, F, G, X],
-or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
 a8 ).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/atp-inputs/u_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/u_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
@@ -4,4 +4,4 @@
 
 %S' c f g x --> c (f x) (g x)
 input_clause(a8,axiom,
-[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
diff -r 66b8455090b8 -r 8606ddd42554 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Sep 21 16:45:53 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Thu Sep 21 17:31:10 2006 +0200
@@ -794,7 +794,8 @@
 
 fun init_funcs_tab funcs = 
     let val tp = !typ_level
-	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC","c_COMBB_e","c_COMBC_e","c_COMBS_e"]
+	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC",
+	                                     "c_COMBB__e","c_COMBC__e","c_COMBS__e"]
 	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs0
 				      | _ => Symtab.update ("hAPP",2) funcs0
 	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1