stripped some legacy
authorhaftmann
Tue Dec 22 15:39:01 2015 +0100 (2015-12-22)
changeset 6191416bfe0a6702d
parent 61913 58b153bfa737
child 61915 e9812a95d108
stripped some legacy
src/HOL/HOL.thy
src/Tools/misc_legacy.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 22 15:38:59 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Dec 22 15:39:01 2015 +0100
     1.3 @@ -1974,8 +1974,8 @@
     1.4        | wrong_prem (Bound _) = true
     1.5        | wrong_prem _ = false;
     1.6      val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
     1.7 +    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp];
     1.8    in
     1.9 -    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    1.10      fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];
    1.11    end;
    1.12  
     2.1 --- a/src/Tools/misc_legacy.ML	Tue Dec 22 15:38:59 2015 +0100
     2.2 +++ b/src/Tools/misc_legacy.ML	Tue Dec 22 15:39:01 2015 +0100
     2.3 @@ -6,13 +6,8 @@
     2.4  signature MISC_LEGACY =
     2.5  sig
     2.6    val add_term_names: term * string list -> string list
     2.7 -  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
     2.8 -  val add_typ_tfree_names: typ * string list -> string list
     2.9 -  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
    2.10    val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
    2.11    val add_term_tfrees: term * (string * sort) list -> (string * sort) list
    2.12 -  val add_term_tfree_names: term * string list -> string list
    2.13 -  val typ_tfrees: typ -> (string * sort) list
    2.14    val typ_tvars: typ -> (indexname * sort) list
    2.15    val term_tfrees: term -> (string * sort) list
    2.16    val term_tvars: term -> (indexname * sort) list
    2.17 @@ -24,7 +19,6 @@
    2.18    val get_def: theory -> xstring -> thm
    2.19    val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic
    2.20    val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm)
    2.21 -  val freeze_thaw: Proof.context -> thm -> thm * (thm -> thm)
    2.22  end;
    2.23  
    2.24  structure Misc_Legacy: MISC_LEGACY =
    2.25 @@ -272,26 +266,4 @@
    2.26           in  (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw)  end
    2.27   end;
    2.28  
    2.29 -(*Basic version of the function above. No option to rename Vars apart in thaw.
    2.30 -  The Frees created from Vars have nice names.*)
    2.31 -fun freeze_thaw ctxt th =
    2.32 - let val fth = Thm.legacy_freezeT th
    2.33 - in
    2.34 -   case Thm.fold_terms Term.add_vars fth [] of
    2.35 -       [] => (fth, fn x => x)
    2.36 -     | vars =>
    2.37 -         let fun newName (ix, _) (pairs, used) =
    2.38 -                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    2.39 -                   in  ((ix,v)::pairs, v::used)  end;
    2.40 -             val (alist, _) =
    2.41 -                 fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
    2.42 -             fun mk_inst (v, T) =
    2.43 -                apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
    2.44 -             val insts = map mk_inst vars
    2.45 -             fun thaw th' =
    2.46 -                 th' |> forall_intr_list (map #2 insts)
    2.47 -                     |> forall_elim_list (map #1 insts)
    2.48 -         in  (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw)  end
    2.49 - end;
    2.50 -
    2.51  end;