src/Tools/nbe.ML
changeset 29272 fb3ccf499df5
parent 28706 3fef773ae6b1
child 30022 1d8b8fa19074
     1.1 --- a/src/Tools/nbe.ML	Wed Dec 31 18:53:16 2008 +0100
     1.2 +++ b/src/Tools/nbe.ML	Wed Dec 31 18:53:17 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Tools/nbe.ML
     1.5 -    ID:         $Id$
     1.6      Authors:    Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen
     1.7  
     1.8  Normalization by evaluation, based on generic code generator.
     1.9 @@ -448,7 +447,7 @@
    1.10        singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    1.11          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    1.12        (TypeInfer.constrain ty t);
    1.13 -    fun check_tvars t = if null (Term.term_tvars t) then t else
    1.14 +    fun check_tvars t = if null (Term.add_tvars t []) then t else
    1.15        error ("Illegal schematic type variables in normalized term: "
    1.16          ^ setmp show_types true (Syntax.string_of_term_global thy) t);
    1.17      val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);