src/Pure/theory.ML
changeset 19806 f860b7a98445
parent 19727 f5895f998402
child 20155 da0505518e69
     1.1 --- a/src/Pure/theory.ML	Wed Jun 07 02:01:27 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Jun 07 02:01:28 2006 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4      val consts = Sign.consts_of thy;
     1.5      fun prep const =
     1.6        let val Const (c, T) = Sign.no_vars pp (Const const)
     1.7 -      in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end;
     1.8 +      in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
     1.9  
    1.10      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
    1.11      val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
    1.12 @@ -267,7 +267,7 @@
    1.13        (case Sign.const_constraint thy c of
    1.14          NONE => error ("Undeclared constant " ^ quote c)
    1.15        | SOME declT => declT);
    1.16 -    val T' = Type.varifyT T;
    1.17 +    val T' = Logic.varifyT T;
    1.18  
    1.19      fun message txt =
    1.20        [Pretty.block [Pretty.str "Specification of constant ",