# HG changeset patch
# User boehmes
# Date 1235718758 -3600
# Node ID a3eebf924eebf70a10abd9a28c45b1c957e21ed3
# Parent  6a874aedb964e8eadeebb69d489067b32766a8f6# Parent  258f9adfdda543dd81f79974b7b2b582f4087847
merged

diff -r 258f9adfdda5 -r a3eebf924eeb src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu Feb 26 15:27:18 2009 -0800
+++ b/src/Pure/conv.ML	Fri Feb 27 08:12:38 2009 +0100
@@ -7,12 +7,17 @@
 infix 1 then_conv;
 infix 0 else_conv;
 
+signature BASIC_CONV =
+sig
+  val then_conv: conv * conv -> conv
+  val else_conv: conv * conv -> conv
+end;
+
 signature CONV =
 sig
+  include BASIC_CONV
   val no_conv: conv
   val all_conv: conv
-  val then_conv: conv * conv -> conv
-  val else_conv: conv * conv -> conv
   val first_conv: conv list -> conv
   val every_conv: conv list -> conv
   val try_conv: conv -> conv
@@ -171,3 +176,6 @@
   | NONE => raise THM ("gconv_rule", i, [th]));
 
 end;
+
+structure BasicConv: BASIC_CONV = Conv;
+open BasicConv;