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