src/Pure/drule.ML

   val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
   val read_instantiate: (string*string)list -> thm -> thm
   val cterm_instantiate: (cterm*cterm)list -> thm -> thm
   val eq_thm_thy: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
-  val weak_eq_thm: thm * thm -> bool
+  val equiv_thm: thm * thm -> bool
   val size_of_thm: thm -> int
   val reflexive_thm: thm
   val symmetric_thm: thm
   val transitive_thm: thm
   val symmetric_fun: thm -> thm

   val goals_conv: (int -> bool) -> (cterm -> thm) -> cterm -> thm
   val fconv_rule: (cterm -> thm) -> thm -> thm
   val norm_hhf_eq: thm
   val is_norm_hhf: term -> bool
   val norm_hhf: theory -> term -> term
+  val unvarify: thm -> thm
   val protect: cterm -> cterm
   val protectI: thm
   val protectD: thm
   val protect_cong: thm
   val implies_intr_protected: cterm list -> thm -> thm

   val sort_triv: theory -> typ * sort -> thm list
   val unconstrainTs: thm -> thm
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
   val rename_bvars: (string * string) list -> thm -> thm
   val rename_bvars': string option list -> thm -> thm
-  val unvarifyT: thm -> thm
-  val unvarify: thm -> thm
   val tvars_intr_list: string list -> thm -> (string * (indexname * sort)) list * thm
   val incr_indexes: thm -> thm -> thm
   val incr_indexes2: thm -> thm -> thm -> thm
   val remdups_rl: thm
   val multi_resolve: thm list -> thm -> thm Seq.seq

 (*Convert all Vars in a theorem to Frees.  Also return a function for
   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
   Similar code in type/freeze_thaw*)
 
 fun freeze_thaw_robust th =
- let val fth = freezeT th
+ let val fth = Thm.freezeT th
      val {prop, tpairs, thy, ...} = rep_thm fth
  in
    case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
        [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
      | vars =>

 
 (*Basic version of the function above. No option to rename Vars apart in thaw.
   The Frees created from Vars have nice names. FIXME: does not check for 
   clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*)
 fun freeze_thaw th =
- let val fth = freezeT th
+ let val fth = Thm.freezeT th
      val {prop, tpairs, thy, ...} = rep_thm fth
  in
    case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
        [] => (fth, fn x => x)
      | vars =>

 (*maintain lists of theorems --- preserving canonical order*)
 val del_rule = remove eq_thm_prop;
 fun add_rule th = cons th o del_rule th;
 val merge_rules = Library.merge eq_thm_prop;
 
-(*weak_eq_thm: ignores variable renaming and (some) type variable renaming*)
-val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);
+(*pattern equivalence*)
+fun equiv_thm ths =
+  Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
 
 
 (*** Meta-Rewriting Rules ***)
 
 fun read_prop s = read_cterm ProtoPure.thy (s, propT);

 
 (*Calling equal_abs_elim with multiple terms*)
 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts);
 
 
+(* global schematic variables *)
+
+fun unvarify th =
+  let
+    val thy = Thm.theory_of_thm th;
+    val cert = Thm.cterm_of thy;
+    val certT = Thm.ctyp_of thy;
+
+    val prop = Thm.full_prop_of th;
+    val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
+      handle TERM (msg, _) => raise THM (msg, 0, [th]);
+
+    val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
+    val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
+    val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
+      let val T' = Term.instantiateT instT0 T
+      in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
+  in Thm.instantiate (instT, inst) th end;
+
+
 (** protected propositions and embedded terms **)
 
 local
   val A = cert (Free ("A", propT));
-  val prop_def = #1 (freeze_thaw ProtoPure.prop_def);
-  val term_def = #1 (freeze_thaw ProtoPure.term_def);
+  val prop_def = unvarify ProtoPure.prop_def;
+  val term_def = unvarify ProtoPure.term_def;
 in
   val protect = Thm.capply (cert Logic.protectC);
   val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard

       ([], prop') => equal_elim (reflexive (cterm_of thy prop')) thm
     | _ => error "More names than abstractions in theorem"
   end;
 
 
-
-(* unvarify(T) *)
-
-(*assume thm in standard form, i.e. no frees, 0 var indexes*)
-
-fun unvarifyT thm =
-  let
-    val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
-    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (tvars_of thm);
-  in instantiate' tfrees [] thm end;
-
-fun unvarify raw_thm =
-  let
-    val thm = unvarifyT raw_thm;
-    val ct = Thm.cterm_of (Thm.theory_of_thm thm);
-    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (vars_of thm);
-  in instantiate' [] frees thm end;
-
-
 (* tvars_intr_list *)
 
 fun tvars_intr_list tfrees thm =
   apfst (map (fn ((s, S), ixn) => (s, (ixn, S)))) (Thm.varifyT'
     (gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm);