# HG changeset patch
# User wenzelm
# Date 1369927271 -7200
# Node ID f76fb8858e0b77268c2bda98fbbbb38900552c84
# Parent  cb15da7bd550dd0bf2857cd48f9558ebd91b657e
tuned signature;
tuned;

diff -r cb15da7bd550 -r f76fb8858e0b src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:10:13 2013 +0200
+++ b/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:21:11 2013 +0200
@@ -23,9 +23,6 @@
 
 signature ISA_ND =
 sig
-  (* inserting meta level params for frees in the conditions *)
-  val allify_conditions: (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
-
   val variant_names: Proof.context -> term list -> string list -> string list
 
   (* meta level fixed params (i.e. !! vars) *)
@@ -40,29 +37,6 @@
 structure IsaND : ISA_ND =
 struct
 
-(* Given ctertmify function, (string,type) pairs capturing the free
-vars that need to be allified in the assumption, and a theorem with
-assumptions possibly containing the free vars, then we give back the
-assumptions allified as hidden hyps.
-
-Given: x
-th: A vs ==> B vs
-Results in: "B vs" [!!x. A x]
-*)
-fun allify_conditions ctermify Ts th =
-  let
-    val premts = Thm.prems_of th;
-
-    fun allify_prem_var (vt as (n, ty)) t =
-      Logic.all_const ty $ Abs (n, ty, Term.abstract_over (Free vt, t))
-
-    val allify_prem = fold_rev allify_prem_var
-
-    val cTs = map (ctermify o Free) Ts
-    val cterm_asms = map (ctermify o allify_prem Ts) premts
-    val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
-  in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
-
 (* 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;
diff -r cb15da7bd550 -r f76fb8858e0b src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 17:10:13 2013 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 17:21:11 2013 +0200
@@ -21,6 +21,28 @@
 structure RW_Inst: RW_INST =
 struct
 
+(* Given (string,type) pairs capturing the free vars that need to be
+allified in the assumption, and a theorem with assumptions possibly
+containing the free vars, then we give back the assumptions allified
+as hidden hyps.
+
+Given: x
+th: A vs ==> B vs
+Results in: "B vs" [!!x. A x]
+*)
+fun allify_conditions Ts th =
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_thm th);
+
+    fun allify (x, T) t =
+      Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
+
+    val cTs = map (cert o Free) Ts;
+    val cterm_asms = map (cert o fold_rev allify Ts) (Thm.prems_of th);
+    val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
+  in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
+
+
 (* Given a list of variables that were bound, and a that has been
 instantiated with free variable placeholders for the bound vars, it
 creates an abstracted version of the theorem, with local bound vars as
@@ -62,7 +84,7 @@
       |> Drule.forall_elim_list tonames;
 
     (* make unconditional rule and prems *)
-    val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule';
+    val (uncond_rule, cprems) = allify_conditions (rev Ts') rule';
 
     (* using these names create lambda-abstracted version of the rule *)
     val abstractions = rev (Ts' ~~ tonames);