src/HOL/Tools/record_package.ML
changeset 30364 577edc39b501
parent 30345 76fd85bbf139
child 30715 e23e15f52d42
     1.1 --- a/src/HOL/Tools/record_package.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -122,7 +122,7 @@
     1.4  (* syntax *)
     1.5  
     1.6  fun prune n xs = Library.drop (n, xs);
     1.7 -fun prefix_base s = NameSpace.map_base_name (fn bname => s ^ bname);
     1.8 +fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname);
     1.9  
    1.10  val Trueprop = HOLogic.mk_Trueprop;
    1.11  fun All xs t = Term.list_all_free (xs, t);
    1.12 @@ -433,8 +433,8 @@
    1.13  fun get_extT_fields thy T =
    1.14    let
    1.15      val ((name,Ts),moreT) = dest_recT T;
    1.16 -    val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
    1.17 -                  in NameSpace.implode (rev (nm::rst)) end;
    1.18 +    val recname = let val (nm::recn::rst) = rev (Long_Name.explode name)
    1.19 +                  in Long_Name.implode (rev (nm::rst)) end;
    1.20      val midx = maxidx_of_typs (moreT::Ts);
    1.21      val varifyT = varifyT midx;
    1.22      val {records,extfields,...} = RecordsData.get thy;
    1.23 @@ -702,7 +702,7 @@
    1.24                       SOME flds
    1.25                       => (let
    1.26                            val (f::fs) = but_last (map fst flds);
    1.27 -                          val flds' = Sign.extern_const thy f :: map NameSpace.base_name fs;
    1.28 +                          val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs;
    1.29                            val (args',more) = split_last args;
    1.30                           in (flds'~~args')@field_lst more end
    1.31                           handle Library.UnequalLengths => [("",t)])
    1.32 @@ -804,7 +804,7 @@
    1.33                             => (let
    1.34                                  val (f :: fs) = but_last flds;
    1.35                                  val flds' = apfst (Sign.extern_const thy) f
    1.36 -                                  :: map (apfst NameSpace.base_name) fs;
    1.37 +                                  :: map (apfst Long_Name.base_name) fs;
    1.38                                  val (args', more) = split_last args;
    1.39                                  val alphavars = map varifyT (but_last alphas);
    1.40                                  val subst = fold2 (curry (Sign.typ_match thy))
    1.41 @@ -1069,7 +1069,7 @@
    1.42               val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy;
    1.43  
    1.44               (*fun mk_abs_var x t = (x, fastype_of t);*)
    1.45 -             fun sel_name u = NameSpace.base_name (unsuffix updateN u);
    1.46 +             fun sel_name u = Long_Name.base_name (unsuffix updateN u);
    1.47  
    1.48               fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
    1.49                    if has_field extfields s (domain_type' mT) then upd else seed s r
    1.50 @@ -1461,7 +1461,7 @@
    1.51            Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
    1.52          val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
    1.53        in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
    1.54 -    val tname = Binding.name (NameSpace.base_name name);
    1.55 +    val tname = Binding.name (Long_Name.base_name name);
    1.56    in
    1.57      thy
    1.58      |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
    1.59 @@ -1475,7 +1475,7 @@
    1.60  
    1.61  fun extension_definition full name fields names alphas zeta moreT more vars thy =
    1.62    let
    1.63 -    val base = NameSpace.base_name;
    1.64 +    val base = Long_Name.base_name;
    1.65      val fieldTs = (map snd fields);
    1.66      val alphas_zeta = alphas@[zeta];
    1.67      val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
    1.68 @@ -1761,7 +1761,7 @@
    1.69      val alphas = map fst args;
    1.70      val name = Sign.full_bname thy bname;
    1.71      val full = Sign.full_bname_path thy bname;
    1.72 -    val base = NameSpace.base_name;
    1.73 +    val base = Long_Name.base_name;
    1.74  
    1.75      val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
    1.76  
    1.77 @@ -1887,11 +1887,11 @@
    1.78  
    1.79      fun parent_more s =
    1.80           if null parents then s
    1.81 -         else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT);
    1.82 +         else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
    1.83  
    1.84      fun parent_more_upd v s =
    1.85        if null parents then v$s
    1.86 -      else let val mp = NameSpace.qualified (#name (List.last parents)) moreN;
    1.87 +      else let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
    1.88             in mk_upd updateN mp v s end;
    1.89  
    1.90      (*record (scheme) type abbreviation*)