replaced ProofContext.infer_types by general Syntax.check_terms;
authorwenzelm
Thu Aug 30 22:35:34 2007 +0200 (2007-08-30)
changeset 24493d4380e9b287b
parent 24492 de3fd08bb41c
child 24494 dc387e3999ec
replaced ProofContext.infer_types by general Syntax.check_terms;
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/res_reconstruct.ML
src/HOLCF/Tools/fixrec_package.ML
src/Pure/Tools/invoke.ML
src/Pure/Tools/nbe.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Aug 30 21:44:29 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Aug 30 22:35:34 2007 +0200
     1.3 @@ -211,7 +211,7 @@
     1.4        list_comb (Const (rec_name, dummyT), fs @ [Free x]))
     1.5      val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
     1.6      val def_prop as _ $ _ $ t =
     1.7 -      singleton (ProofContext.infer_types (ProofContext.init thy))
     1.8 +      singleton (Syntax.check_terms (ProofContext.init thy))
     1.9          (Logic.mk_equals (Const (fname, dummyT), rhs));
    1.10    in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end;
    1.11  
     2.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Aug 30 21:44:29 2007 +0200
     2.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Aug 30 22:35:34 2007 +0200
     2.3 @@ -367,7 +367,7 @@
     2.4  
     2.5  (*For Isabelle, the lhs of a definition must be a constant.*)
     2.6  fun mk_const_def sign (c, Ty, rhs) =
     2.7 -  singleton (ProofContext.infer_types (ProofContext.init sign))
     2.8 +  singleton (Syntax.check_terms (ProofContext.init sign))
     2.9      (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
    2.10  
    2.11  (*Make all TVars available for instantiation by adding a ? to the front*)
     3.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Aug 30 21:44:29 2007 +0200
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Aug 30 22:35:34 2007 +0200
     3.3 @@ -227,7 +227,7 @@
     3.4                                  fs @ map Bound (0 ::(length ls downto 1))))
     3.5      val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
     3.6      val def_prop =
     3.7 -      singleton (ProofContext.infer_types (ProofContext.init thy))
     3.8 +      singleton (Syntax.check_terms (ProofContext.init thy))
     3.9          (Logic.mk_equals (Const (fname, dummyT), rhs));
    3.10    in (def_name, def_prop) end;
    3.11  
     4.1 --- a/src/HOL/Tools/res_reconstruct.ML	Thu Aug 30 21:44:29 2007 +0200
     4.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Thu Aug 30 22:35:34 2007 +0200
     4.3 @@ -238,7 +238,7 @@
     4.4    vt0 holds the initial sort constraints, from the conjecture clauses.*)
     4.5  fun clause_of_strees ctxt vt0 ts =
     4.6    let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
     4.7 -    singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
     4.8 +    singleton (Syntax.check_terms ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
     4.9    end;
    4.10  
    4.11  (*Quantification over a list of Vars. FIXME: for term.ML??*)
     5.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Thu Aug 30 21:44:29 2007 +0200
     5.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Thu Aug 30 22:35:34 2007 +0200
     5.3 @@ -21,7 +21,7 @@
     5.4  (* legacy type inference *)
     5.5  
     5.6  fun legacy_infer_term thy t =
     5.7 -  singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t);
     5.8 +  singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
     5.9  
    5.10  fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT);
    5.11  
     6.1 --- a/src/Pure/Tools/invoke.ML	Thu Aug 30 21:44:29 2007 +0200
     6.2 +++ b/src/Pure/Tools/invoke.ML	Thu Aug 30 22:35:34 2007 +0200
     6.3 @@ -99,7 +99,7 @@
     6.4    end;
     6.5  
     6.6  fun infer_terms ctxt =
     6.7 -  ProofContext.infer_types ctxt o
     6.8 +  Syntax.check_terms ctxt o
     6.9      (map (fn (t, T) => TypeInfer.constrain t (TypeInfer.paramify_vars T)));
    6.10  
    6.11  in
     7.1 --- a/src/Pure/Tools/nbe.ML	Thu Aug 30 21:44:29 2007 +0200
     7.2 +++ b/src/Pure/Tools/nbe.ML	Thu Aug 30 22:35:34 2007 +0200
     7.3 @@ -137,7 +137,7 @@
     7.4          ^ setmp show_types true (Sign.string_of_term thy) t);
     7.5      val ty = type_of t;
     7.6      fun constrain t =
     7.7 -      singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
     7.8 +      singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain t ty);
     7.9      val _ = ensure_funs thy funcgr t;
    7.10    in
    7.11      t
     8.1 --- a/src/Tools/nbe.ML	Thu Aug 30 21:44:29 2007 +0200
     8.2 +++ b/src/Tools/nbe.ML	Thu Aug 30 22:35:34 2007 +0200
     8.3 @@ -323,7 +323,7 @@
     8.4        subst_Frees (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []))
     8.5        #> subst_Vars (map (fn (ixn, T) => (ixn, Var (ixn, T))) (Term.add_vars t []))
     8.6      fun constrain t =
     8.7 -      singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
     8.8 +      singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain t ty);
     8.9      fun check_tvars t = if null (Term.term_tvars t) then t else
    8.10        error ("Illegal schematic type variables in normalized term: "
    8.11          ^ setmp show_types true (Sign.string_of_term thy) t);