# HG changeset patch
# User wenzelm
# Date 1129651169 -7200
# Node ID 66902148c436e02dac50923d383bd126c175ea3a
# Parent  6274b426594bf60612dc9f9327989ede2fca1a45
functor: no Simplifier argument;
Simplifier.theory_context;

diff -r 6274b426594b -r 66902148c436 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Tue Oct 18 17:59:28 2005 +0200
+++ b/src/Provers/hypsubst.ML	Tue Oct 18 17:59:29 2005 +0200
@@ -33,7 +33,6 @@
 
 signature HYPSUBST_DATA =
   sig
-  structure Simplifier : SIMPLIFIER
   val dest_Trueprop    : term -> term
   val dest_eq          : term -> term*term*typ
   val dest_imp         : term -> term*term
@@ -69,7 +68,7 @@
 
 exception EQ_VAR;
 
-fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
+fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
 
 (*Simplifier turns Bound variables to special Free variables:
   change it back (any Bound variable will do)*)
@@ -132,18 +131,20 @@
       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
     handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
 
-local open Simplifier
+local
 in
 
   (*Select a suitable equality assumption; substitute throughout the subgoal
     If bnd is true, then it replaces Bound variables only. *)
   fun gen_hyp_subst_tac bnd =
-    let val tac = SUBGOAL (fn (Bi, i) =>
-      let val (k, _) = eq_var bnd true Bi
-          val hyp_subst_ss = empty_ss setmksimps (mk_eqs bnd)
+    let fun tac i st = SUBGOAL (fn (Bi, _) =>
+      let
+        val (k, _) = eq_var bnd true Bi
+        val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
+          setmksimps (mk_eqs bnd)
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]
-      end handle THM _ => no_tac | EQ_VAR => no_tac)
+      end handle THM _ => no_tac | EQ_VAR => no_tac) i st
     in REPEAT_DETERM1 o tac end;
 
 end;