# HG changeset patch
# User wenzelm
# Date 1136557100 -3600
# Node ID 04b9f2bf5a480f2b3fb20c161019c415a84512e1
# Parent  f6a553aa3d815690da24eaf6876a331173578fb8
tuned EqSubst setup;

diff -r f6a553aa3d81 -r 04b9f2bf5a48 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Jan 06 15:18:19 2006 +0100
+++ b/src/FOL/FOL.thy	Fri Jan 06 15:18:20 2006 +0100
@@ -52,7 +52,7 @@
 use "~~/src/Provers/eqsubst.ML";
 use "eqrule_FOL_data.ML";
 
-setup EQSubstTac.setup
+setup EqSubst.setup
 
 
 subsection {* Other simple lemmas *}
diff -r f6a553aa3d81 -r 04b9f2bf5a48 src/FOL/eqrule_FOL_data.ML
--- a/src/FOL/eqrule_FOL_data.ML	Fri Jan 06 15:18:19 2006 +0100
+++ b/src/FOL/eqrule_FOL_data.ML	Fri Jan 06 15:18:20 2006 +0100
@@ -1,5 +1,5 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      sys/eqrule_FOL_data.ML
+(*  ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Created:    18 Feb 2004
@@ -51,7 +51,5 @@
        o zero_var_indexes)
 
 end;
-structure EqRuleData = ZF_EqRuleData;
 
-structure EQSubstTac = 
-  EQSubstTacFUN(structure EqRuleData = EqRuleData);
+structure EqSubst = EqSubstFun(ZF_EqRuleData);
diff -r f6a553aa3d81 -r 04b9f2bf5a48 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jan 06 15:18:19 2006 +0100
+++ b/src/HOL/HOL.thy	Fri Jan 06 15:18:20 2006 +0100
@@ -1194,7 +1194,7 @@
 
 use "~~/src/Provers/eqsubst.ML";
 use "eqrule_HOL_data.ML";
-setup EQSubstTac.setup
+setup EqSubst.setup
 
 
 subsubsection {* Code generator setup *}
diff -r f6a553aa3d81 -r 04b9f2bf5a48 src/HOL/eqrule_HOL_data.ML
--- a/src/HOL/eqrule_HOL_data.ML	Fri Jan 06 15:18:19 2006 +0100
+++ b/src/HOL/eqrule_HOL_data.ML	Fri Jan 06 15:18:20 2006 +0100
@@ -1,6 +1,5 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      HOL/eqrule_HOL_data.ML
-    Id:		$Id$
+(*  ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Modified:   22 July 2004
@@ -61,9 +60,4 @@
 
 end;
 
-structure EqRuleData = HOL_EqRuleData;
-
-structure EQSubstTac = 
-  EQSubstTacFUN(structure EqRuleData = EqRuleData);
-
-
+structure EqSubst = EqSubstFun(HOL_EqRuleData);
diff -r f6a553aa3d81 -r 04b9f2bf5a48 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Fri Jan 06 15:18:19 2006 +0100
+++ b/src/Provers/eqsubst.ML	Fri Jan 06 15:18:20 2006 +0100
@@ -27,7 +27,7 @@
 
 
 (* the signature of an instance of the SQSUBST tactic *)
-signature EQSUBST_TAC =
+signature EQSUBST =
 sig
 
   exception eqsubst_occL_exp of
@@ -124,9 +124,8 @@
 end;
 
 
-functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA)
-  : EQSUBST_TAC
-= struct
+functor EqSubstFun (EqRuleData : EQRULE_DATA): EQSUBST =
+struct
 
   (* a type abriviation for match information *)
   type match =