1.1 --- a/src/Pure/Isar/locale.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Dec 05 18:42:37 2008 +0100
     1.3 @@ -646,7 +646,7 @@
     1.4        | unify _ env = env;
     1.5      val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
     1.6      val Vs = map (Option.map (Envir.norm_type unifier)) Us';
     1.7 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
     1.8 +    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
     1.9    in map (Option.map (Envir.norm_type unifier')) Vs end;
    1.10  
    1.11  fun params_of elemss =
    1.12 @@ -711,7 +711,7 @@
    1.13        (Vartab.empty, maxidx);
    1.14  
    1.15      val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
    1.16 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
    1.17 +    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
    1.18  
    1.19      fun inst_parms (i, ps) =
    1.20        List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
    1.21 @@ -1100,15 +1100,15 @@
    1.22  *)
    1.23  
    1.24  fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
    1.25 -        val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
    1.26 +        val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
    1.27        in
    1.28          ((ids',
    1.29           merge_syntax ctxt ids'
    1.30 -           (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
    1.31 +           (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
    1.32             handle Symtab.DUP x => err_in_locale ctxt
    1.33               ("Conflicting syntax for parameter: " ^ quote x)
    1.34               (map #1 ids')),
    1.35 -         [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
    1.36 +         [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
    1.37        end
    1.38    | flatten _ ((ids, syn), Elem elem) =
    1.39        ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
    1.40 @@ -1252,7 +1252,7 @@
    1.41  
    1.42  
    1.43  fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
    1.44 -      let val x = Name.name_of b
    1.45 +      let val x = Binding.base_name b
    1.46        in (b, AList.lookup (op =) parms x, mx) end) fixes)
    1.47    | finish_ext_elem parms _ (Constrains _, _) = Constrains []
    1.48    | finish_ext_elem _ close (Assumes asms, propp) =