simplified TypeInfer.infer_types;
authorwenzelm
Wed Jun 18 22:32:03 2008 +0200 (2008-06-18 ago)
changeset 27264843472ae2116
parent 27263 a6b7f934fbc4
child 27265 49c81f6d7a08
simplified TypeInfer.infer_types;
src/Pure/Isar/proof_context.ML
src/Tools/nbe.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jun 18 22:32:02 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jun 18 22:32:03 2008 +0200
     1.3 @@ -579,8 +579,7 @@
     1.4    let val Mode {pattern, ...} = get_mode ctxt in
     1.5      TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
     1.6        (try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern)
     1.7 -      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts)
     1.8 -    |> #1 |> map #1
     1.9 +      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
    1.10      handle TYPE (msg, _, _) => error msg
    1.11    end;
    1.12  
     2.1 --- a/src/Tools/nbe.ML	Wed Jun 18 22:32:02 2008 +0200
     2.2 +++ b/src/Tools/nbe.ML	Wed Jun 18 22:32:03 2008 +0200
     2.3 @@ -385,11 +385,10 @@
     2.4        (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
     2.5      val type_frees = Term.map_aterms
     2.6        (fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t);
     2.7 -    fun type_infer t = [(t, ty)]
     2.8 -      |> TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
     2.9 -           (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE)
    2.10 -           Name.context 0 NONE
    2.11 -      |> fst |> the_single |> fst;
    2.12 +    fun type_infer t =
    2.13 +      singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    2.14 +        (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    2.15 +      (TypeInfer.constrain ty t);
    2.16      fun check_tvars t = if null (Term.term_tvars t) then t else
    2.17        error ("Illegal schematic type variables in normalized term: "
    2.18          ^ setmp show_types true (Syntax.string_of_term_global thy) t);