--- 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
--- 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 *)