--- a/src/HOL/Tools/Meson/meson.ML Mon Mar 19 20:32:57 2012 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Mon Mar 19 21:10:33 2012 +0100
@@ -752,7 +752,7 @@
(*Converting one theorem from a disjunction to a meta-level clause*)
fun make_meta_clause th =
- let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
+ let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th
in
(zero_var_indexes o Thm.varifyT_global o thaw 0 o
negated_asm_of_head o make_horn resolution_clause_rules) fth
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Mar 19 20:32:57 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Mar 19 21:10:33 2012 +0100
@@ -374,7 +374,7 @@
do_formula pos body_t
#> (if also_skolems andalso will_surely_be_skolemized then
add_pconst_to_table true
- (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
+ (Misc_Legacy.gensym skolem_prefix, PType (order_of_type abs_T, []))
else
I)
and do_term_or_formula ext_arg T =
--- a/src/Pure/drule.ML Mon Mar 19 20:32:57 2012 +0100
+++ b/src/Pure/drule.ML Mon Mar 19 21:10:33 2012 +0100
@@ -20,8 +20,6 @@
val forall_elim_list: cterm list -> thm -> thm
val gen_all: thm -> thm
val lift_all: cterm -> thm -> thm
- val legacy_freeze_thaw: thm -> thm * (thm -> thm)
- val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
@@ -299,52 +297,6 @@
#> Thm.close_derivation;
-(*Convert all Vars in a theorem to Frees. Also return a function for
- reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*)
-
-fun legacy_freeze_thaw_robust th =
- let val fth = Thm.legacy_freezeT th
- val thy = Thm.theory_of_thm fth
- in
- case Thm.fold_terms Term.add_vars fth [] of
- [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
- | vars =>
- let fun newName (ix,_) = (ix, legacy_gensym (string_of_indexname ix))
- val alist = map newName vars
- fun mk_inst (v,T) =
- (cterm_of thy (Var(v,T)),
- cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
- val insts = map mk_inst vars
- fun thaw i th' = (*i is non-negative increment for Var indexes*)
- th' |> forall_intr_list (map #2 insts)
- |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
- in (Thm.instantiate ([],insts) fth, thaw) end
- end;
-
-(*Basic version of the function above. No option to rename Vars apart in thaw.
- The Frees created from Vars have nice names.*)
-fun legacy_freeze_thaw th =
- let val fth = Thm.legacy_freezeT th
- val thy = Thm.theory_of_thm fth
- in
- case Thm.fold_terms Term.add_vars fth [] of
- [] => (fth, fn x => x)
- | vars =>
- let fun newName (ix, _) (pairs, used) =
- let val v = singleton (Name.variant_list used) (string_of_indexname ix)
- in ((ix,v)::pairs, v::used) end;
- val (alist, _) =
- fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
- fun mk_inst (v, T) =
- (cterm_of thy (Var(v,T)),
- cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
- val insts = map mk_inst vars
- fun thaw th' =
- th' |> forall_intr_list (map #2 insts)
- |> forall_elim_list (map #1 insts)
- in (Thm.instantiate ([],insts) fth, thaw) end
- end;
-
(*Rotates a rule's premises to the left by k*)
fun rotate_prems 0 = I
| rotate_prems k = Thm.permute_prems 0 k;
--- a/src/Pure/library.ML Mon Mar 19 20:32:57 2012 +0100
+++ b/src/Pure/library.ML Mon Mar 19 21:10:33 2012 +0100
@@ -213,7 +213,6 @@
'a -> 'b -> 'c * 'b
val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
- val legacy_gensym: string -> string
type serial = int
val serial: unit -> serial
val serial_string: unit -> string
@@ -1043,27 +1042,6 @@
in part end;
-
-(* generating identifiers -- often fresh *)
-
-local
-(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
-fun gensym_char i =
- if i<26 then chr (ord "A" + i)
- else if i<52 then chr (ord "a" + i - 26)
- else chr (ord "0" + i - 52);
-
-val char_vec = Vector.tabulate (62, gensym_char);
-fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
-
-val gensym_seed = Unsynchronized.ref (0: int);
-
-in
- fun legacy_gensym pre =
- pre ^ newid (NAMED_CRITICAL "legacy_gensym" (fn () => Unsynchronized.inc gensym_seed));
-end;
-
-
(* serial numbers and abstract stamps *)
type serial = int;
--- a/src/Tools/misc_legacy.ML Mon Mar 19 20:32:57 2012 +0100
+++ b/src/Tools/misc_legacy.ML Mon Mar 19 21:10:33 2012 +0100
@@ -23,6 +23,9 @@
val mk_defpair: term * term -> string * term
val get_def: theory -> xstring -> thm
val METAHYPS: (thm list -> tactic) -> int -> tactic
+ val gensym: string -> string
+ val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
+ val freeze_thaw: thm -> thm * (thm -> thm)
end;
structure Misc_Legacy: MISC_LEGACY =
@@ -229,5 +232,71 @@
end;
+
+(* generating identifiers -- often fresh *)
+
+local
+(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
+fun gensym_char i =
+ if i<26 then chr (ord "A" + i)
+ else if i<52 then chr (ord "a" + i - 26)
+ else chr (ord "0" + i - 52);
+
+val char_vec = Vector.tabulate (62, gensym_char);
+fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
+
+val gensym_seed = Unsynchronized.ref (0: int);
+
+in
+ fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
end;
+
+(*Convert all Vars in a theorem to Frees. Also return a function for
+ reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*)
+
+fun freeze_thaw_robust th =
+ let val fth = Thm.legacy_freezeT th
+ val thy = Thm.theory_of_thm fth
+ in
+ case Thm.fold_terms Term.add_vars fth [] of
+ [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
+ | vars =>
+ let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
+ val alist = map newName vars
+ fun mk_inst (v,T) =
+ (cterm_of thy (Var(v,T)),
+ cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
+ val insts = map mk_inst vars
+ fun thaw i th' = (*i is non-negative increment for Var indexes*)
+ th' |> forall_intr_list (map #2 insts)
+ |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
+ in (Thm.instantiate ([],insts) fth, thaw) end
+ end;
+
+(*Basic version of the function above. No option to rename Vars apart in thaw.
+ The Frees created from Vars have nice names.*)
+fun freeze_thaw th =
+ let val fth = Thm.legacy_freezeT th
+ val thy = Thm.theory_of_thm fth
+ in
+ case Thm.fold_terms Term.add_vars fth [] of
+ [] => (fth, fn x => x)
+ | vars =>
+ let fun newName (ix, _) (pairs, used) =
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
+ in ((ix,v)::pairs, v::used) end;
+ val (alist, _) =
+ fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
+ fun mk_inst (v, T) =
+ (cterm_of thy (Var(v,T)),
+ cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
+ val insts = map mk_inst vars
+ fun thaw th' =
+ th' |> forall_intr_list (map #2 insts)
+ |> forall_elim_list (map #1 insts)
+ in (Thm.instantiate ([],insts) fth, thaw) end
+ end;
+
+end;
+