# HG changeset patch
# User wenzelm
# Date 1369927561 -7200
# Node ID 54c0d4128b30fa5e0d00fc3b6717bbd6995a7692
# Parent  f76fb8858e0b77268c2bda98fbbbb38900552c84
tuned signature;

diff -r f76fb8858e0b -r 54c0d4128b30 src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:21:11 2013 +0200
+++ b/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:26:01 2013 +0200
@@ -28,8 +28,6 @@
   (* meta level fixed params (i.e. !! vars) *)
   val fix_alls_term: Proof.context -> int -> term -> term * term list
 
-  val unfix_frees: cterm list -> thm -> thm
-
   (* assumptions/subgoals *)
   val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm)
 end
@@ -37,10 +35,6 @@
 structure IsaND : ISA_ND =
 struct
 
-(* make free vars into schematic vars with index zero *)
-fun unfix_frees frees =
-   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
-
 (* datatype to capture an exported result, ie a fix or assume. *)
 datatype export =
   Export of
diff -r f76fb8858e0b -r 54c0d4128b30 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Thu May 30 17:21:11 2013 +0200
+++ b/src/Tools/eqsubst.ML	Thu May 30 17:26:01 2013 +0200
@@ -56,6 +56,10 @@
 fun prep_meta_eq ctxt =
   Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
 
+(* make free vars into schematic vars with index zero *)
+fun unfix_frees frees =
+   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
+
 
 type match =
   ((indexname * (sort * typ)) list (* type instantiations *)
@@ -246,7 +250,7 @@
 (* rule is the equation for substitution *)
 fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
   RW_Inst.rw ctxt m rule conclthm
-  |> IsaND.unfix_frees cfvs
+  |> unfix_frees cfvs
   |> Conv.fconv_rule Drule.beta_eta_conversion
   |> (fn r => Tactic.rtac r i st);
 
@@ -326,7 +330,7 @@
       RW_Inst.rw ctxt m rule pth
       |> (Seq.hd o prune_params_tac)
       |> Thm.permute_prems 0 ~1 (* put old asm first *)
-      |> IsaND.unfix_frees cfvs (* unfix any global params *)
+      |> unfix_frees cfvs (* unfix any global params *)
       |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
   in
     (* ~j because new asm starts at back, thus we subtract 1 *)