# HG changeset patch
# User lcp
# Date 797158975 -7200
# Node ID 70676af0ac974e0a1a03cac8b3dece113224536b
# Parent  6413adca76014b354030218e37f6fa8ba5a80d6c
Set up for new hyp_subst_tac.

diff -r 6413adca7601 -r 70676af0ac97 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Thu Apr 06 11:01:13 1995 +0200
+++ b/src/FOL/ROOT.ML	Thu Apr 06 11:02:55 1995 +0200
@@ -16,18 +16,20 @@
 print_depth 1;  
 use_thy "FOL";
 
-use "../Provers/hypsubst.ML";
-use "../Provers/classical.ML";
 use "../Provers/simplifier.ML";
 use "../Provers/splitter.ML";
 use "../Provers/ind.ML";
+use "../Provers/hypsubst.ML";
+use "../Provers/classical.ML";
 
 (*** Applying HypsubstFun to generate hyp_subst_tac ***)
 
 structure Hypsubst_Data =
   struct
-  (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
+  structure Simplifier = Simplifier
+    (*Take apart an equality judgement; otherwise raise Match!*)
+  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u)
+  val eq_reflection = eq_reflection
   val imp_intr = impI
   val rev_mp = rev_mp
   val subst = subst