src/Pure/Isar/locale.ML
changeset 29275 9fa69e3858d6
parent 29269 5c25a2012975
child 29363 c1f024b4d76d
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 31 18:53:18 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 31 18:53:19 2008 +0100
     1.3 @@ -714,7 +714,7 @@
     1.4      val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
     1.5  
     1.6      fun inst_parms (i, ps) =
     1.7 -      List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
     1.8 +      List.foldr OldTerm.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 @@ -1791,10 +1791,11 @@
    1.13      val name = Sign.full_bname thy bname;
    1.14  
    1.15      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
    1.16 -    val env = Term.add_term_free_names (body, []);
    1.17 +    val env = Term.add_free_names body [];
    1.18      val xs = filter (member (op =) env o #1) parms;
    1.19      val Ts = map #2 xs;
    1.20 -    val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
    1.21 +    val extraTs =
    1.22 +      (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
    1.23        |> Library.sort_wrt #1 |> map TFree;
    1.24      val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
    1.25  
    1.26 @@ -1949,8 +1950,8 @@
    1.27      val elemss = import_elemss @ body_elemss |>
    1.28        map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
    1.29  
    1.30 -    val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
    1.31 -      List.foldr Term.add_typ_tfrees [] (map snd parms);
    1.32 +    val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\
    1.33 +      List.foldr OldTerm.add_typ_tfrees [] (map snd parms);
    1.34      val _ = if null extraTs then ()
    1.35        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    1.36