src/Pure/Isar/specification.ML
changeset 37145 01aa36932739
parent 36610 bafd82950e24
child 37216 3165bc303f66
     1.1 --- a/src/Pure/Isar/specification.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -96,13 +96,13 @@
     1.4        (case duplicates (op =) commons of [] => ()
     1.5        | dups => error ("Duplicate local variables " ^ commas_quote dups));
     1.6      val frees = rev ((fold o fold_aterms) add_free As (rev commons));
     1.7 -    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
     1.8 +    val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
     1.9      val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
    1.10  
    1.11      fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
    1.12        | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
    1.13        | abs_body lev y (t as Free (x, T)) =
    1.14 -          if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
    1.15 +          if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
    1.16            else t
    1.17        | abs_body _ _ a = a;
    1.18      fun close (y, U) B =