# HG changeset patch # User wenzelm # Date 1322832403 -3600 # Node ID 0430f9123e439aa2938a0b6feaf1593865db614d # Parent e77eba3cb2e11b598d1ea096b7dbb2c732173bd9 eliminated some legacy operations; diff -r e77eba3cb2e1 -r 0430f9123e43 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Fri Dec 02 13:59:25 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Dec 02 14:26:43 2011 +0100 @@ -83,8 +83,7 @@ else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs; val arities = remove (op =) 0 (Datatype_Aux.get_arities descr'); val unneeded_vars = - subtract (op =) - (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars); + subtract (op =) (fold Term.add_tfree_namesT (leafTs' @ branchTs) []) (hd tyvars); val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars; val recTs = Datatype_Aux.get_rec_types descr' sorts; @@ -386,7 +385,7 @@ val prop = Thm.prop_of thm; val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop; - val used = Misc_Legacy.add_term_tfree_names (a, []); + val used = Term.add_tfree_names a []; fun mk_thm i = let @@ -708,7 +707,7 @@ let val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts'; val _ = - (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of + (case subtract (op =) tvs (fold Term.add_tfree_namesT cargs' []) of [] => () | vs => error ("Extra type variables on rhs: " ^ commas vs)); val c = Sign.full_name_path tmp_thy (Binding.name_of tname) cname; diff -r e77eba3cb2e1 -r 0430f9123e43 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Dec 02 13:59:25 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Dec 02 14:26:43 2011 +0100 @@ -95,7 +95,7 @@ val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr' sorts; - val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs; + val used = fold Term.add_tfree_namesT recTs []; val newTs = take (length (hd descr)) recTs; val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); @@ -292,7 +292,7 @@ val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr' sorts; - val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs; + val used = fold Term.add_tfree_namesT recTs []; val newTs = take (length (hd descr)) recTs; val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS); diff -r e77eba3cb2e1 -r 0430f9123e43 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 02 13:59:25 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 02 14:26:43 2011 +0100 @@ -139,12 +139,12 @@ else pair NONE; val flt = if null indnames then I - else filter (fn Free (s, _) => member (op =) indnames s | _ => false); + else filter (member (op =) indnames o fst); fun abstr (t1, t2) = (case t1 of NONE => - (case flt (Misc_Legacy.term_frees t2) of - [Free (s, T)] => SOME (absfree (s, T) t2) + (case flt (Term.add_frees t2 []) of + [(s, T)] => SOME (absfree (s, T) t2) | _ => NONE) | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2)))); val insts = diff -r e77eba3cb2e1 -r 0430f9123e43 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Dec 02 13:59:25 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Dec 02 14:26:43 2011 +0100 @@ -371,9 +371,9 @@ fun strip_case'' dest (pat, rhs) = (case dest (Term.add_free_names pat []) rhs of SOME (exp as Free _, clauses) => - if member op aconv (Misc_Legacy.term_frees pat) exp andalso + if Term.exists_subterm (curry (op aconv) exp) pat andalso not (exists (fn (_, rhs') => - member op aconv (Misc_Legacy.term_frees rhs') exp) clauses) + Term.exists_subterm (curry (op aconv) exp) rhs') clauses) then maps (strip_case'' dest) (map (fn (pat', rhs') => (subst_free [(exp, pat')] pat, rhs')) clauses) diff -r e77eba3cb2e1 -r 0430f9123e43 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Dec 02 13:59:25 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Dec 02 14:26:43 2011 +0100 @@ -406,7 +406,7 @@ Syntax.string_of_typ ctxt T); fun type_of_constr (cT as (_, T)) = let - val frees = Misc_Legacy.typ_tfrees T; + val frees = Term.add_tfreesT T []; val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T)) handle TYPE _ => no_constr cT val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else (); diff -r e77eba3cb2e1 -r 0430f9123e43 src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Dec 02 13:59:25 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Dec 02 14:26:43 2011 +0100 @@ -217,7 +217,7 @@ let val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr' sorts; - val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs; + val used = fold Term.add_tfree_namesT recTs []; val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used; @@ -269,7 +269,7 @@ let val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr' sorts; - val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs; + val used = fold Term.add_tfree_namesT recTs []; val newTs = take (length (hd descr)) recTs; val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS); @@ -316,7 +316,7 @@ let val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr' sorts; - val used' = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs; + val used' = fold Term.add_tfree_namesT recTs []; val newTs = take (length (hd descr)) recTs; val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS); val P = Free ("P", T' --> HOLogic.boolT);