eliminated some legacy operations;
authorwenzelm
Fri Dec 02 15:23:27 2011 +0100 (2011-12-02)
changeset 45741088256c289e7
parent 45740 132a3e1c0fe5
child 45742 debb68e8d23f
eliminated some legacy operations;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 14:54:25 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 15:23:27 2011 +0100
     1.3 @@ -1414,7 +1414,7 @@
     1.4  
     1.5      val _ = warning "defining recursion combinator ...";
     1.6  
     1.7 -    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
     1.8 +    val used = fold Term.add_tfree_namesT recTs [];
     1.9  
    1.10      val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
    1.11  
     2.1 --- a/src/HOL/Statespace/state_space.ML	Fri Dec 02 14:54:25 2011 +0100
     2.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Dec 02 15:23:27 2011 +0100
     2.3 @@ -470,7 +470,7 @@
     2.4    let
     2.5      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     2.6      val T = Syntax.read_typ ctxt' raw_T;
     2.7 -    val env' = Misc_Legacy.add_typ_tfrees (T, env);
     2.8 +    val env' = Term.add_tfreesT T env;
     2.9    in (T, env') end;
    2.10  
    2.11  fun cert_typ ctxt raw_T env =
    2.12 @@ -478,7 +478,7 @@
    2.13      val thy = Proof_Context.theory_of ctxt;
    2.14      val T = Type.no_tvars (Sign.certify_typ thy raw_T)
    2.15        handle TYPE (msg, _, _) => error msg;
    2.16 -    val env' = Misc_Legacy.add_typ_tfrees (T, env);
    2.17 +    val env' = Term.add_tfreesT T env;
    2.18    in (T, env') end;
    2.19  
    2.20  fun gen_define_statespace prep_typ state_space args name parents comps thy =
     3.1 --- a/src/HOL/Tools/record.ML	Fri Dec 02 14:54:25 2011 +0100
     3.2 +++ b/src/HOL/Tools/record.ML	Fri Dec 02 15:23:27 2011 +0100
     3.3 @@ -1495,7 +1495,7 @@
     3.4    let
     3.5      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     3.6      val T = Syntax.read_typ ctxt' raw_T;
     3.7 -    val env' = Misc_Legacy.add_typ_tfrees (T, env);
     3.8 +    val env' = Term.add_tfreesT T env;
     3.9    in (T, env') end;
    3.10  
    3.11  fun cert_typ ctxt raw_T env =
    3.12 @@ -1503,7 +1503,7 @@
    3.13      val thy = Proof_Context.theory_of ctxt;
    3.14      val T = Type.no_tvars (Sign.certify_typ thy raw_T)
    3.15        handle TYPE (msg, _, _) => error msg;
    3.16 -    val env' = Misc_Legacy.add_typ_tfrees (T, env);
    3.17 +    val env' = Term.add_tfreesT T env;
    3.18    in (T, env') end;
    3.19  
    3.20  
     4.1 --- a/src/HOL/Tools/refute.ML	Fri Dec 02 14:54:25 2011 +0100
     4.2 +++ b/src/HOL/Tools/refute.ML	Fri Dec 02 15:23:27 2011 +0100
     4.3 @@ -403,8 +403,7 @@
     4.4  
     4.5  fun close_form t =
     4.6    let
     4.7 -    (* (Term.indexname * Term.typ) list *)
     4.8 -    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
     4.9 +    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
    4.10    in
    4.11      fold (fn ((x, i), T) => fn t' =>
    4.12        Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
    4.13 @@ -1212,8 +1211,7 @@
    4.14        error "Term to be refuted contains schematic type variables"
    4.15  
    4.16      (* existential closure over schematic variables *)
    4.17 -    (* (Term.indexname * Term.typ) list *)
    4.18 -    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
    4.19 +    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
    4.20      (* Term.term *)
    4.21      val ex_closure = fold (fn ((x, i), T) => fn t' =>
    4.22        HOLogic.exists_const T $