# HG changeset patch
# User berghofe
# Date 899233066 -7200
# Node ID 866a281a8c2a0f2c041a750a115c66557d39e23f
# Parent  8c782c25a11ecd942d5d3c117ca4ba9d1e56fb00
Removed structure Prod_Syntax.

diff -r 8c782c25a11e -r 866a281a8c2a TFL/post.sml
--- a/TFL/post.sml	Tue Jun 30 20:51:15 1998 +0200
+++ b/TFL/post.sml	Tue Jun 30 20:57:46 1998 +0200
@@ -168,7 +168,7 @@
 
 
 (*lcp: curry the predicate of the induction rule*)
-fun curry_rule rl = Prod_Syntax.split_rule_var
+fun curry_rule rl = split_rule_var
                         (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
 			 rl);