# HG changeset patch
# User wenzelm
# Date 877001597 -7200
# Node ID 5423e06b9fe617f2a9ba1d0736550c46ed35886a
# Parent  acc1347cf2a088ec5a7949f25d987f4fd7ce7ce1
fixed merge_theories;

diff -r acc1347cf2a0 -r 5423e06b9fe6 src/Cube/Cube.ML
--- a/src/Cube/Cube.ML	Thu Oct 16 13:28:04 1997 +0200
+++ b/src/Cube/Cube.ML	Thu Oct 16 13:33:17 1997 +0200
@@ -35,7 +35,7 @@
 val pi_bb = get_axiom Lomega_thy "pi_bb";
 val Lomega = simple @ [lam_bb,pi_bb];
 
-val LOmega_thy = merge_theories(L2_thy,Lomega_thy);
+val LOmega_thy = merge_theories "LOmega" (L2_thy,Lomega_thy);
 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
 
 val LP_thy =
@@ -50,11 +50,11 @@
 val pi_sb = get_axiom LP_thy "pi_sb";
 val LP = simple @ [lam_sb,pi_sb];
 
-val LP2_thy = merge_theories(L2_thy,LP_thy);
+val LP2_thy = merge_theories "LP2" (L2_thy,LP_thy);
 val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];
 
-val LPomega_thy = merge_theories(LP_thy,Lomega_thy);
+val LPomega_thy = merge_theories "LPomega" (LP_thy,Lomega_thy);
 val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];
 
-val CC_thy = merge_theories(L2_thy,LPomega_thy);
+val CC_thy = merge_theories "CC" (L2_thy,LPomega_thy);
 val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];