src/Pure/Isar/locale.ML
changeset 23178 07ba6b58b3d2
parent 22846 fb79144af9a3
child 23228 05fb9b2b16d7
     1.1 --- a/src/Pure/Isar/locale.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -664,7 +664,7 @@
     1.4      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
     1.5  
     1.6      fun inst_parms (i, ps) =
     1.7 -      foldr Term.add_typ_tfrees [] (map_filter snd ps)
     1.8 +      List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
     1.9        |> map_filter (fn (a, S) =>
    1.10            let val T = Envir.norm_type unifier' (TVar ((a, i), S))
    1.11            in if T = TFree (a, S) then NONE else SOME (a, T) end)
    1.12 @@ -1707,7 +1707,7 @@
    1.13      val env = Term.add_term_free_names (body, []);
    1.14      val xs = filter (member (op =) env o #1) parms;
    1.15      val Ts = map #2 xs;
    1.16 -    val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
    1.17 +    val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
    1.18        |> Library.sort_wrt #1 |> map TFree;
    1.19      val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
    1.20  
    1.21 @@ -1855,8 +1855,8 @@
    1.22          map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
    1.23      val imports = prep_expr thy raw_imports;
    1.24  
    1.25 -    val extraTs = foldr Term.add_term_tfrees [] exts' \\
    1.26 -      foldr Term.add_typ_tfrees [] (map snd parms);
    1.27 +    val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
    1.28 +      List.foldr Term.add_typ_tfrees [] (map snd parms);
    1.29      val _ = if null extraTs then ()
    1.30        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    1.31