# HG changeset patch
# User boehmes
# Date 1235667608 -3600
# Node ID 6a874aedb964e8eadeebb69d489067b32766a8f6
# Parent  0726792e1726588ce34946a912df1fbe6cb7540f
Made then_conv and else_conv available as infix operations.

diff -r 0726792e1726 -r 6a874aedb964 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu Feb 26 17:42:43 2009 +0100
+++ b/src/Pure/conv.ML	Thu Feb 26 18:00:08 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;