src/Pure/sign.ML
changeset 35845 e5980f0ad025
parent 35801 952308389b8b
child 35988 76ca601c941e
     1.1 --- a/src/Pure/sign.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -441,7 +441,7 @@
     1.4          val c = full_name thy b;
     1.5          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
     1.6            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
     1.7 -        val T' = Logic.varifyT T;
     1.8 +        val T' = Logic.varifyT_global T;
     1.9        in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
    1.10      val args = map prep raw_args;
    1.11    in
    1.12 @@ -486,7 +486,7 @@
    1.13  fun add_const_constraint (c, opt_T) thy =
    1.14    let
    1.15      fun prepT raw_T =
    1.16 -      let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T)))
    1.17 +      let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T)))
    1.18        in cert_term thy (Const (c, T)); T end
    1.19        handle TYPE (msg, _, _) => error msg;
    1.20    in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;