--- a/src/HOL/cladata.ML Wed Nov 12 12:24:55 1997 +0100
+++ b/src/HOL/cladata.ML Wed Nov 12 12:30:15 1997 +0100
@@ -26,6 +26,9 @@
structure Hypsubst = HypsubstFun(Hypsubst_Data);
open Hypsubst;
+val thin_refl = prove_goal HOL.thy
+ "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
+
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
@@ -33,7 +36,8 @@
val mp = mp
val not_elim = notE
val classical = classical
- val hyp_subst_tacs=[hyp_subst_tac]
+ val thin_refl = thin_refl
+ val hyp_subst_tacs= [REPEAT_DETERM o ematch_tac [thin_refl] THEN' hyp_subst_tac]
end;
structure Classical = ClassicalFun(Classical_Data);