--- 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 *}
--- 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);
--- 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 *}
--- 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);
--- 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 =