# HG changeset patch
# User dixon
# Date 1114540719 -7200
# Node ID 55e443aa711dcec0f973a32dff96e7d1686490e7
# Parent  1ae0a47dcccde5c6a18fdb00add93bf887fea4e7
lucas - updated to reflect isand.ML update

diff -r 1ae0a47dcccd -r 55e443aa711d src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Tue Apr 26 20:38:15 2005 +0200
+++ b/src/Provers/eqsubst.ML	Tue Apr 26 20:38:39 2005 +0200
@@ -208,7 +208,7 @@
 (* rule is the equation for substitution *)
 fun apply_subst_in_concl i th (cfvs, conclthm) rule m = 
     (RWInst.rw m rule conclthm)
-      |> IsaND.schemify_frees_to_vars cfvs
+      |> IsaND.unfix_frees cfvs
       |> RWInst.beta_eta_contract_tac
       |> (fn r => Tactic.rtac r i th);
 
@@ -280,7 +280,7 @@
 fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = 
     (RWInst.rw m rule pth)
       |> Thm.permute_prems 0 ~1
-      |> IsaND.schemify_frees_to_vars cfvs
+      |> IsaND.unfix_frees cfvs
       |> RWInst.beta_eta_contract_tac
       |> (fn r => Tactic.dtac r i th);