src/HOL/Tools/record.ML
changeset 35239 0dfec017bc83
parent 35232 f588e1169c8b
child 35240 663436ed5bd6
     1.1 --- a/src/HOL/Tools/record.ML	Fri Feb 19 20:41:34 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Feb 19 21:31:14 2010 +0100
     1.3 @@ -145,16 +145,15 @@
     1.4        rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
     1.5      val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
     1.6      val isomT = fastype_of body;
     1.7 -    val isom_bind = Binding.name (name ^ isoN);
     1.8 -    val isom_name = Sign.full_name typ_thy isom_bind;
     1.9 +    val isom_binding = Binding.name (name ^ isoN);
    1.10 +    val isom_name = Sign.full_name typ_thy isom_binding;
    1.11      val isom = Const (isom_name, isomT);
    1.12 -    val isom_spec = (Thm.def_name (name ^ isoN), Logic.mk_equals (isom, body));
    1.13  
    1.14      val ([isom_def], cdef_thy) =
    1.15        typ_thy
    1.16 -      |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
    1.17 +      |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
    1.18        |> PureThy.add_defs false
    1.19 -        [Thm.no_attributes (apfst (Binding.conceal o Binding.name) isom_spec)];
    1.20 +        [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
    1.21  
    1.22      val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
    1.23      val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
    1.24 @@ -162,7 +161,7 @@
    1.25      val thm_thy =
    1.26        cdef_thy
    1.27        |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
    1.28 -      |> Sign.parent_path
    1.29 +      |> Sign.restore_naming thy
    1.30        |> Code.add_default_eqn isom_def;
    1.31    in
    1.32      ((isom, cons $ isom), thm_thy)
    1.33 @@ -280,11 +279,9 @@
    1.34  
    1.35  (* constructor *)
    1.36  
    1.37 -fun mk_extC (name, T) Ts = (suffix extN name, Ts ---> T);
    1.38 -
    1.39  fun mk_ext (name, T) ts =
    1.40    let val Ts = map fastype_of ts
    1.41 -  in list_comb (Const (mk_extC (name, T) Ts), ts) end;
    1.42 +  in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
    1.43  
    1.44  
    1.45  (* selector *)
    1.46 @@ -802,10 +799,7 @@
    1.47                    let
    1.48                      val (args, rest) = split_args (map fst (but_last fields)) fargs;
    1.49                      val more' = mk_ext rest;
    1.50 -                  in
    1.51 -                    (* FIXME authentic syntax *)
    1.52 -                    list_comb (Syntax.const (suffix extN ext), args @ [more'])
    1.53 -                  end
    1.54 +                  in list_comb (Syntax.const (Syntax.constN ^ ext ^ extN), args @ [more']) end
    1.55                | NONE => err ("no fields defined for " ^ ext))
    1.56            | NONE => err (name ^ " is no proper field"))
    1.57        | mk_ext [] = more;
    1.58 @@ -850,8 +844,9 @@
    1.59  
    1.60  local
    1.61  
    1.62 -fun field_updates_tr' (tm as Const (c, _) $ k $ u) =
    1.63 +fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
    1.64        let
    1.65 +        val extern = Consts.extern (ProofContext.consts_of ctxt);
    1.66          val t =
    1.67            (case k of
    1.68              Abs (_, _, Abs (_, _, t) $ Bound 0) =>
    1.69 @@ -860,18 +855,19 @@
    1.70                if null (loose_bnos t) then t else raise Match
    1.71            | _ => raise Match);
    1.72        in
    1.73 -        (case try (unsuffix updateN) c of
    1.74 -          SOME name =>
    1.75 -            (* FIXME check wrt. record data (??) *)
    1.76 -            (* FIXME early extern (!??) *)
    1.77 -            apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
    1.78 -              (field_updates_tr' u)
    1.79 +        (case try (unprefix Syntax.constN) c |> Option.map extern of
    1.80 +          SOME update_name =>
    1.81 +            (case try (unsuffix updateN) update_name of
    1.82 +              SOME name =>
    1.83 +                apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
    1.84 +                  (field_updates_tr' ctxt u)
    1.85 +            | NONE => ([], tm))
    1.86          | NONE => ([], tm))
    1.87        end
    1.88 -  | field_updates_tr' tm = ([], tm);
    1.89 -
    1.90 -fun record_update_tr' tm =
    1.91 -  (case field_updates_tr' tm of
    1.92 +  | field_updates_tr' _ tm = ([], tm);
    1.93 +
    1.94 +fun record_update_tr' ctxt tm =
    1.95 +  (case field_updates_tr' ctxt tm of
    1.96      ([], _) => raise Match
    1.97    | (ts, u) =>
    1.98        Syntax.const @{syntax_const "_record_update"} $ u $
    1.99 @@ -881,10 +877,9 @@
   1.100  
   1.101  fun field_update_tr' name =
   1.102    let
   1.103 -    (* FIXME authentic syntax *)
   1.104 -    val update_name = suffix updateN name;
   1.105 -    fun tr' [t, u] = record_update_tr' (Syntax.const update_name $ t $ u)
   1.106 -      | tr' _ = raise Match;
   1.107 +    val update_name = Syntax.constN ^ name ^ updateN;
   1.108 +    fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
   1.109 +      | tr' _ _ = raise Match;
   1.110    in (update_name, tr') end;
   1.111  
   1.112  end;
   1.113 @@ -892,26 +887,25 @@
   1.114  
   1.115  local
   1.116  
   1.117 -(* FIXME early extern (!??) *)
   1.118  (* FIXME Syntax.free (??) *)
   1.119  fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
   1.120 -
   1.121  fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
   1.122  
   1.123  fun record_tr' ctxt t =
   1.124    let
   1.125      val thy = ProofContext.theory_of ctxt;
   1.126 +    val extern = Consts.extern (ProofContext.consts_of ctxt);
   1.127  
   1.128      fun strip_fields t =
   1.129        (case strip_comb t of
   1.130          (Const (ext, _), args as (_ :: _)) =>
   1.131 -          (case try (unsuffix extN) (Sign.intern_const thy ext) of  (* FIXME authentic syntax *)
   1.132 +          (case try (unprefix Syntax.constN o unsuffix extN) ext of
   1.133              SOME ext' =>
   1.134                (case get_extfields thy ext' of
   1.135                  SOME fields =>
   1.136                   (let
   1.137                      val f :: fs = but_last (map fst fields);
   1.138 -                    val fields' = Sign.extern_const thy f :: map Long_Name.base_name fs;
   1.139 +                    val fields' = extern f :: map Long_Name.base_name fs;
   1.140                      val (args', more) = split_last args;
   1.141                    in (fields' ~~ args') @ strip_fields more end
   1.142                    handle Library.UnequalLengths => [("", t)])
   1.143 @@ -932,7 +926,7 @@
   1.144  
   1.145  fun record_ext_tr' name =
   1.146    let
   1.147 -    val ext_name = suffix extN name;
   1.148 +    val ext_name = Syntax.constN ^ name ^ extN;
   1.149      fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
   1.150    in (ext_name, tr') end;
   1.151  
   1.152 @@ -1573,7 +1567,7 @@
   1.153            (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
   1.154          | _ => false);
   1.155  
   1.156 -    fun is_all t =
   1.157 +    fun is_all t =  (* FIXME *)
   1.158        (case t of
   1.159          Const (quantifier, _) $ _ =>
   1.160            if quantifier = @{const_name all} orelse quantifier = @{const_name All} then ~1 else 0
   1.161 @@ -1662,27 +1656,30 @@
   1.162  
   1.163  fun extension_definition name fields alphas zeta moreT more vars thy =
   1.164    let
   1.165 -    val base = Long_Name.base_name;
   1.166 +    val base_name = Long_Name.base_name name;
   1.167 +
   1.168      val fieldTs = map snd fields;
   1.169 +    val fields_moreTs = fieldTs @ [moreT];
   1.170 +
   1.171      val alphas_zeta = alphas @ [zeta];
   1.172      val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
   1.173 -    val extT_name = suffix ext_typeN name
   1.174 -    val extT = Type (extT_name, alphas_zetaTs);
   1.175 -    val fields_moreTs = fieldTs @ [moreT];
   1.176 -
   1.177 -
   1.178 -    (*before doing anything else, create the tree of new types
   1.179 -      that will back the record extension*)
   1.180 +
   1.181 +    val ext_binding = Binding.name (suffix extN base_name);
   1.182 +    val ext_name = suffix extN name;
   1.183 +    val extT = Type (suffix ext_typeN name, alphas_zetaTs);
   1.184 +    val ext_type = fields_moreTs ---> extT;
   1.185 +
   1.186 +
   1.187 +    (* the tree of new types that will back the record extension *)
   1.188  
   1.189      val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
   1.190  
   1.191      fun mk_iso_tuple (left, right) (thy, i) =
   1.192        let
   1.193          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   1.194 -        val nm = suffix suff (Long_Name.base_name name);
   1.195 -        val ((_, cons), thy') =
   1.196 -          Iso_Tuple_Support.add_iso_tuple_type
   1.197 -            (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   1.198 +        val ((_, cons), thy') = thy
   1.199 +          |> Iso_Tuple_Support.add_iso_tuple_type
   1.200 +            (suffix suff base_name, alphas_zeta) (fastype_of left, fastype_of right);
   1.201        in
   1.202          (cons $ left $ right, (thy', i + 1))
   1.203        end;
   1.204 @@ -1720,19 +1717,15 @@
   1.205  
   1.206      (* prepare declarations and definitions *)
   1.207  
   1.208 -    (*fields constructor*)
   1.209 -    val ext_decl = mk_extC (name, extT) fields_moreTs;
   1.210 -    val ext_spec = list_comb (Const ext_decl, vars @ [more]) :== ext_body;
   1.211 -
   1.212 -    fun mk_ext args = list_comb (Const ext_decl, args);
   1.213 -
   1.214 -
   1.215      (* 1st stage part 2: define the ext constant *)
   1.216  
   1.217 +    fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
   1.218 +    val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
   1.219 +
   1.220      fun mk_defs () =
   1.221        typ_thy
   1.222 -      |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)]
   1.223 -      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)]
   1.224 +      |> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd
   1.225 +      |> PureThy.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
   1.226        ||> Theory.checkpoint
   1.227      val ([ext_def], defs_thy) =
   1.228        timeit_msg "record extension constructor def:" mk_defs;
   1.229 @@ -1856,7 +1849,7 @@
   1.230  fun obj_to_meta_all thm =
   1.231    let
   1.232      fun E thm =  (* FIXME proper name *)
   1.233 -      (case (SOME (spec OF [thm]) handle THM _ => NONE) of
   1.234 +      (case SOME (spec OF [thm]) handle THM _ => NONE of
   1.235          SOME thm' => E thm'
   1.236        | NONE => thm);
   1.237      val th1 = E thm;
   1.238 @@ -1876,16 +1869,12 @@
   1.239  
   1.240  (* record_definition *)
   1.241  
   1.242 -fun record_definition (args, b) parent (parents: parent_info list) raw_fields thy =
   1.243 +fun record_definition (args, binding) parent (parents: parent_info list) raw_fields thy =
   1.244    let
   1.245 -    val external_names = Name_Space.external_names (Sign.naming_of thy);
   1.246 -
   1.247      val alphas = map fst args;
   1.248  
   1.249 -    val base_name = Binding.name_of b;   (* FIXME include qualifier etc. (!?) *)
   1.250 -    val name = Sign.full_name thy b;
   1.251 -    val full = Sign.full_name_path thy base_name;
   1.252 -    val base = Long_Name.base_name;
   1.253 +    val name = Sign.full_name thy binding;
   1.254 +    val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
   1.255  
   1.256      val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
   1.257      val field_syntax = map #3 raw_fields;
   1.258 @@ -1895,13 +1884,13 @@
   1.259      val parent_names = map fst parent_fields;
   1.260      val parent_types = map snd parent_fields;
   1.261      val parent_fields_len = length parent_fields;
   1.262 -    val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
   1.263 +    val parent_variants =
   1.264 +      Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
   1.265      val parent_vars = ListPair.map Free (parent_variants, parent_types);
   1.266      val parent_len = length parents;
   1.267  
   1.268      val fields = map (apfst full) bfields;
   1.269      val names = map fst fields;
   1.270 -    val extN = full b;
   1.271      val types = map snd fields;
   1.272      val alphas_fields = fold Term.add_tfree_namesT types [];
   1.273      val alphas_ext = inter (op =) alphas_fields alphas;
   1.274 @@ -1931,18 +1920,20 @@
   1.275      val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
   1.276  
   1.277  
   1.278 -    (* 1st stage: extension_thy *)
   1.279 -
   1.280 -    val ((extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), extension_thy) =
   1.281 +    (* 1st stage: ext_thy *)
   1.282 +
   1.283 +    val extension_name = full binding;
   1.284 +
   1.285 +    val ((extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
   1.286        thy
   1.287 -      |> Sign.add_path base_name
   1.288 -      |> extension_definition extN fields alphas_ext zeta moreT more vars;
   1.289 +      |> Sign.qualified_path false binding
   1.290 +      |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
   1.291  
   1.292      val _ = timing_msg "record preparing definitions";
   1.293      val Type extension_scheme = extT;
   1.294      val extension_name = unsuffix ext_typeN (fst extension_scheme);
   1.295      val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
   1.296 -    val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
   1.297 +    val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
   1.298      val extension_id = implode extension_names;
   1.299  
   1.300      fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
   1.301 @@ -1978,13 +1969,9 @@
   1.302      val w = Free (wN, rec_schemeT 0)
   1.303  
   1.304  
   1.305 -    (* prepare print translation functions *)
   1.306 -    (* FIXME authentic syntax *)
   1.307 -
   1.308 -    val field_update_tr's =
   1.309 -      map field_update_tr' (distinct (op =) (maps external_names (full_moreN :: names)));
   1.310 -
   1.311 -    val record_ext_tr's = map record_ext_tr' (external_names extN);
   1.312 +    (* print translations *)
   1.313 +
   1.314 +    val external_names = Name_Space.external_names (Sign.naming_of ext_thy);
   1.315  
   1.316      val record_ext_type_abbr_tr's =
   1.317        let
   1.318 @@ -1995,9 +1982,13 @@
   1.319      val record_ext_type_tr's =
   1.320        let
   1.321          (*avoid conflict with record_type_abbr_tr's*)
   1.322 -        val trnames = if parent_len > 0 then external_names extN else [];
   1.323 +        val trnames = if parent_len > 0 then external_names extension_name else [];
   1.324        in map record_ext_type_tr' trnames end;
   1.325  
   1.326 +    val advanced_print_translation =
   1.327 +      map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
   1.328 +      record_ext_type_tr's @ record_ext_type_abbr_tr's;
   1.329 +
   1.330  
   1.331      (* prepare declarations *)
   1.332  
   1.333 @@ -2013,8 +2004,8 @@
   1.334  
   1.335      (*record (scheme) type abbreviation*)
   1.336      val recordT_specs =
   1.337 -      [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, NoSyn),
   1.338 -        (b, alphas, recT0, NoSyn)];
   1.339 +      [(Binding.suffix_name schemeN binding, alphas @ [zeta], rec_schemeT0, NoSyn),
   1.340 +        (binding, alphas, recT0, NoSyn)];
   1.341  
   1.342      val ext_defs = ext_def :: map #ext_def parents;
   1.343  
   1.344 @@ -2035,8 +2026,8 @@
   1.345              fun to_Var (Free (c, T)) = Var ((c, 1), T);
   1.346            in mk_rec (map to_Var all_vars_more) 0 end;
   1.347  
   1.348 -        val cterm_rec = cterm_of extension_thy r_rec0;
   1.349 -        val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
   1.350 +        val cterm_rec = cterm_of ext_thy r_rec0;
   1.351 +        val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
   1.352          val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
   1.353          val init_thm = named_cterm_instantiate insts updacc_eq_triv;
   1.354          val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   1.355 @@ -2057,10 +2048,10 @@
   1.356      (*selectors*)
   1.357      fun mk_sel_spec ((c, T), thm) =
   1.358        let
   1.359 -        val acc $ arg =
   1.360 -          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm;
   1.361 +        val (acc $ arg, _) =
   1.362 +          HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
   1.363          val _ =
   1.364 -          if (arg aconv r_rec0) then ()
   1.365 +          if arg aconv r_rec0 then ()
   1.366            else raise TERM ("mk_sel_spec: different arg", [arg]);
   1.367        in
   1.368          Const (mk_selC rec_schemeT0 (c, T)) :== acc
   1.369 @@ -2070,8 +2061,8 @@
   1.370      (*updates*)
   1.371      fun mk_upd_spec ((c, T), thm) =
   1.372        let
   1.373 -        val upd $ _ $ arg =
   1.374 -          fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (concl_of thm))));
   1.375 +        val (upd $ _ $ arg, _) =
   1.376 +          HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
   1.377          val _ =
   1.378            if arg aconv r_rec0 then ()
   1.379            else raise TERM ("mk_sel_spec: different arg", [arg]);
   1.380 @@ -2096,17 +2087,15 @@
   1.381      (* 2st stage: defs_thy *)
   1.382  
   1.383      fun mk_defs () =
   1.384 -      extension_thy
   1.385 -      |> Sign.add_trfuns ([], [], field_update_tr's, [])
   1.386 -      |> Sign.add_advanced_trfuns
   1.387 -        ([], [], record_ext_tr's @ record_ext_type_tr's @ record_ext_type_abbr_tr's, [])
   1.388 -      |> Sign.parent_path
   1.389 +      ext_thy
   1.390 +      |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
   1.391 +      |> Sign.restore_naming thy
   1.392        |> Sign.add_tyabbrs_i recordT_specs
   1.393 -      |> Sign.add_path base_name
   1.394 -      |> Sign.add_consts_i
   1.395 -          (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx)) sel_decls (field_syntax @ [NoSyn]))
   1.396 -      |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, NoSyn)))
   1.397 -          (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   1.398 +      |> Sign.qualified_path false binding
   1.399 +      |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx))
   1.400 +        (sel_decls ~~ (field_syntax @ [NoSyn]))
   1.401 +      |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn))
   1.402 +        (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   1.403        |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
   1.404          sel_specs
   1.405        ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
   1.406 @@ -2137,9 +2126,9 @@
   1.407      (*updates*)
   1.408      fun mk_upd_prop (i, (c, T)) =
   1.409        let
   1.410 -        val x' = Free (Name.variant all_variants (base c ^ "'"), T --> T);
   1.411 +        val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
   1.412          val n = parent_fields_len + i;
   1.413 -        val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more
   1.414 +        val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
   1.415        in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
   1.416      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   1.417  
   1.418 @@ -2401,7 +2390,7 @@
   1.419        |> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
   1.420        |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
   1.421        |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
   1.422 -      |> Sign.parent_path;
   1.423 +      |> Sign.restore_naming thy;
   1.424  
   1.425    in final_thy end;
   1.426  
   1.427 @@ -2411,12 +2400,12 @@
   1.428  (*We do all preparations and error checks here, deferring the real
   1.429    work to record_definition.*)
   1.430  fun gen_add_record prep_typ prep_raw_parent quiet_mode
   1.431 -    (params, b) raw_parent raw_fields thy =
   1.432 +    (params, binding) raw_parent raw_fields thy =
   1.433    let
   1.434      val _ = Theory.requires thy "Record" "record definitions";
   1.435      val _ =
   1.436        if quiet_mode then ()
   1.437 -      else writeln ("Defining record " ^ quote (Binding.name_of b) ^ " ...");
   1.438 +      else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
   1.439  
   1.440      val ctxt = ProofContext.init thy;
   1.441  
   1.442 @@ -2456,7 +2445,7 @@
   1.443  
   1.444      (* errors *)
   1.445  
   1.446 -    val name = Sign.full_name thy b;
   1.447 +    val name = Sign.full_name thy binding;
   1.448      val err_dup_record =
   1.449        if is_none (get_record thy name) then []
   1.450        else ["Duplicate definition of record " ^ quote name];
   1.451 @@ -2493,9 +2482,9 @@
   1.452  
   1.453      val _ = if null errs then () else error (cat_lines errs);
   1.454    in
   1.455 -    thy |> record_definition (args, b) parent parents bfields
   1.456 +    thy |> record_definition (args, binding) parent parents bfields
   1.457    end
   1.458 -  handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of b));
   1.459 +  handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
   1.460  
   1.461  val add_record = gen_add_record cert_typ (K I);
   1.462  val add_record_cmd = gen_add_record read_typ read_raw_parent;