src/HOL/Tools/record.ML
changeset 35262 9ea4445d2ccf
parent 35240 663436ed5bd6
child 35363 09489d8ffece
     1.1 --- a/src/HOL/Tools/record.ML	Sun Feb 21 21:41:29 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sun Feb 21 22:35:02 2010 +0100
     1.3 @@ -799,7 +799,7 @@
     1.4                    let
     1.5                      val (args, rest) = split_args (map fst (but_last fields)) fargs;
     1.6                      val more' = mk_ext rest;
     1.7 -                  in list_comb (Syntax.const (Syntax.constN ^ ext ^ extN), args @ [more']) end
     1.8 +                  in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
     1.9                | NONE => err ("no fields defined for " ^ ext))
    1.10            | NONE => err (name ^ " is no proper field"))
    1.11        | mk_ext [] = more;
    1.12 @@ -977,7 +977,7 @@
    1.13      fun strip_fields t =
    1.14        (case strip_comb t of
    1.15          (Const (ext, _), args as (_ :: _)) =>
    1.16 -          (case try (unprefix Syntax.constN o unsuffix extN) ext of
    1.17 +          (case try (Syntax.unmark_const o unsuffix extN) ext of
    1.18              SOME ext' =>
    1.19                (case get_extfields thy ext' of
    1.20                  SOME fields =>
    1.21 @@ -1004,7 +1004,7 @@
    1.22  
    1.23  fun record_ext_tr' name =
    1.24    let
    1.25 -    val ext_name = Syntax.constN ^ name ^ extN;
    1.26 +    val ext_name = Syntax.mark_const (name ^ extN);
    1.27      fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
    1.28    in (ext_name, tr') end;
    1.29  
    1.30 @@ -1024,7 +1024,7 @@
    1.31                if null (loose_bnos t) then t else raise Match
    1.32            | _ => raise Match);
    1.33        in
    1.34 -        (case try (unprefix Syntax.constN) c |> Option.map extern of
    1.35 +        (case Option.map extern (try Syntax.unmark_const c) of
    1.36            SOME update_name =>
    1.37              (case try (unsuffix updateN) update_name of
    1.38                SOME name =>
    1.39 @@ -1046,7 +1046,7 @@
    1.40  
    1.41  fun field_update_tr' name =
    1.42    let
    1.43 -    val update_name = Syntax.constN ^ name ^ updateN;
    1.44 +    val update_name = Syntax.mark_const (name ^ updateN);
    1.45      fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
    1.46        | tr' _ _ = raise Match;
    1.47    in (update_name, tr') end;