# HG changeset patch
# User wenzelm
# Date 1305366163 -7200
# Node ID 4e33894aec6dd37ba72e595d37fc654b5556e6ef
# Parent  02c88bdabe752c992500e6c7fc60d7aecaa36396
modernized functor names;
tuned;

diff -r 02c88bdabe75 -r 4e33894aec6d src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOL/FOL.thy	Sat May 14 11:42:43 2011 +0200
@@ -167,7 +167,7 @@
 section {* Classical Reasoner *}
 
 ML {*
-structure Cla = ClassicalFun
+structure Cla = Classical
 (
   val imp_elim = @{thm imp_elim}
   val not_elim = @{thm notE}
diff -r 02c88bdabe75 -r 4e33894aec6d src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOL/IFOL.thy	Sat May 14 11:42:43 2011 +0200
@@ -19,7 +19,6 @@
   "~~/src/Tools/project_rule.ML"
   "~~/src/Tools/atomize_elim.ML"
   ("fologic.ML")
-  ("hypsubstdata.ML")
   ("intprover.ML")
 begin
 
@@ -592,7 +591,23 @@
 
 lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" .
 
-use "hypsubstdata.ML"
+ML {*
+structure Hypsubst = Hypsubst
+(
+  val dest_eq = FOLogic.dest_eq
+  val dest_Trueprop = FOLogic.dest_Trueprop
+  val dest_imp = FOLogic.dest_imp
+  val eq_reflection = @{thm eq_reflection}
+  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
+  val imp_intr = @{thm impI}
+  val rev_mp = @{thm rev_mp}
+  val subst = @{thm subst}
+  val sym = @{thm sym}
+  val thin_refl = @{thm thin_refl}
+);
+open Hypsubst;
+*}
+
 setup hypsubst_setup
 use "intprover.ML"
 
diff -r 02c88bdabe75 -r 4e33894aec6d src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOL/IsaMakefile	Sat May 14 11:42:43 2011 +0200
@@ -36,8 +36,7 @@
   $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
   $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
   $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
-  document/root.tex fologic.ML hypsubstdata.ML intprover.ML		\
-  simpdata.ML
+  document/root.tex fologic.ML intprover.ML simpdata.ML
 	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
 
 
diff -r 02c88bdabe75 -r 4e33894aec6d src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Sat May 14 00:32:16 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-
-(** Applying HypsubstFun to generate hyp_subst_tac **)
-structure Hypsubst_Data =
-struct
-  structure Simplifier = Simplifier
-  val dest_eq = FOLogic.dest_eq
-  val dest_Trueprop = FOLogic.dest_Trueprop
-  val dest_imp = FOLogic.dest_imp
-  val eq_reflection = @{thm eq_reflection}
-  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
-  val imp_intr = @{thm impI}
-  val rev_mp = @{thm rev_mp}
-  val subst = @{thm subst}
-  val sym = @{thm sym}
-  val thin_refl = @{thm thin_refl}
-end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-open Hypsubst;
diff -r 02c88bdabe75 -r 4e33894aec6d src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOLP/FOLP.thy	Sat May 14 11:42:43 2011 +0200
@@ -103,17 +103,14 @@
 use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
 
 ML {*
-(*** Applying ClassicalFun to create a classical prover ***)
-structure Classical_Data =
-struct
+structure Cla = Classical
+(
   val sizef = size_of_thm
   val mp = @{thm mp}
   val not_elim = @{thm notE}
   val swap = @{thm swap}
   val hyp_subst_tacs = [hyp_subst_tac]
-end;
-
-structure Cla = ClassicalFun(Classical_Data);
+);
 open Cla;
 
 (*Propositional rules
diff -r 02c88bdabe75 -r 4e33894aec6d src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOLP/IFOLP.thy	Sat May 14 11:42:43 2011 +0200
@@ -587,11 +587,8 @@
 use "hypsubst.ML"
 
 ML {*
-
-(*** Applying HypsubstFun to generate hyp_subst_tac ***)
-
-structure Hypsubst_Data =
-struct
+structure Hypsubst = Hypsubst
+(
   (*Take apart an equality judgement; otherwise raise Match!*)
   fun dest_eq (Const (@{const_name Proof}, _) $
     (Const (@{const_name eq}, _)  $ t $ u) $ _) = (t, u);
@@ -605,9 +602,7 @@
   val subst = @{thm subst}
   val sym = @{thm sym}
   val thin_refl = @{thm thin_refl}
-end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
+);
 open Hypsubst;
 *}
 
diff -r 02c88bdabe75 -r 4e33894aec6d src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOLP/classical.ML	Sat May 14 11:42:43 2011 +0200
@@ -60,7 +60,7 @@
   end;
 
 
-functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
+functor Classical(Data: CLASSICAL_DATA): CLASSICAL = 
 struct
 
 local open Data in
diff -r 02c88bdabe75 -r 4e33894aec6d src/FOLP/hypsubst.ML
--- a/src/FOLP/hypsubst.ML	Sat May 14 00:32:16 2011 +0200
+++ b/src/FOLP/hypsubst.ML	Sat May 14 11:42:43 2011 +0200
@@ -26,7 +26,7 @@
   val inspect_pair        : bool -> term * term -> thm
   end;
 
-functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
+functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
 struct
 
 local open Data in
diff -r 02c88bdabe75 -r 4e33894aec6d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 14 00:32:16 2011 +0200
+++ b/src/HOL/HOL.thy	Sat May 14 11:42:43 2011 +0200
@@ -826,9 +826,8 @@
   "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
 
 ML {*
-structure Hypsubst = HypsubstFun(
-struct
-  structure Simplifier = Simplifier
+structure Hypsubst = Hypsubst
+(
   val dest_eq = HOLogic.dest_eq
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
@@ -839,18 +838,18 @@
   val subst = @{thm subst}
   val sym = @{thm sym}
   val thin_refl = @{thm thin_refl};
-end);
+);
 open Hypsubst;
 
-structure Classical = ClassicalFun(
-struct
+structure Classical = Classical
+(
   val imp_elim = @{thm imp_elim}
   val not_elim = @{thm notE}
   val swap = @{thm swap}
   val classical = @{thm classical}
   val sizef = Drule.size_of_thm
   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
-end);
+);
 
 structure Basic_Classical: BASIC_CLASSICAL = Classical; 
 open Basic_Classical;
diff -r 02c88bdabe75 -r 4e33894aec6d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat May 14 00:32:16 2011 +0200
+++ b/src/Provers/classical.ML	Sat May 14 11:42:43 2011 +0200
@@ -131,7 +131,7 @@
 end;
 
 
-functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
+functor Classical(Data: CLASSICAL_DATA): CLASSICAL =
 struct
 
 (** classical elimination rules **)
diff -r 02c88bdabe75 -r 4e33894aec6d src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sat May 14 00:32:16 2011 +0200
+++ b/src/Provers/hypsubst.ML	Sat May 14 11:42:43 2011 +0200
@@ -53,7 +53,7 @@
   val hypsubst_setup         : theory -> theory
 end;
 
-functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
+functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
 struct
 
 exception EQ_VAR;