use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
authorwenzelm
Thu Mar 19 13:28:55 2009 +0100 (2009-03-19 ago)
changeset 305856b2ba4666336
parent 30584 7e839627b9e7
child 30586 9674f64a0702
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
src/Pure/Isar/class.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Mar 19 13:26:19 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Mar 19 13:28:55 2009 +0100
     1.3 @@ -236,7 +236,7 @@
     1.4          thy
     1.5          |> Sign.declare_const [] ((b, ty0), syn)
     1.6          |> snd
     1.7 -        |> pair ((Binding.name_of b, ty), (c, ty'))
     1.8 +        |> pair ((Name.of_binding b, ty), (c, ty'))
     1.9        end;
    1.10    in
    1.11      thy
     2.1 --- a/src/Pure/Isar/constdefs.ML	Thu Mar 19 13:26:19 2009 +0100
     2.2 +++ b/src/Pure/Isar/constdefs.ML	Thu Mar 19 13:28:55 2009 +0100
     2.3 @@ -36,7 +36,7 @@
     2.4      val prop = prep_prop var_ctxt raw_prop;
     2.5      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
     2.6      val _ =
     2.7 -      (case Option.map Binding.name_of d of
     2.8 +      (case Option.map Name.of_binding d of
     2.9          NONE => ()
    2.10        | SOME c' =>
    2.11            if c <> c' then
     3.1 --- a/src/Pure/Isar/element.ML	Thu Mar 19 13:26:19 2009 +0100
     3.2 +++ b/src/Pure/Isar/element.ML	Thu Mar 19 13:28:55 2009 +0100
     3.3 @@ -96,7 +96,7 @@
     3.4  fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
     3.5    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
     3.6     | Constrains xs => Constrains (xs |> map (fn (x, T) =>
     3.7 -      (Binding.name_of (binding (Binding.name x)), typ T)))
     3.8 +      (Name.of_binding (binding (Binding.name x)), typ T)))
     3.9     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
    3.10        ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
    3.11     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
     4.1 --- a/src/Pure/Isar/expression.ML	Thu Mar 19 13:26:19 2009 +0100
     4.2 +++ b/src/Pure/Isar/expression.ML	Thu Mar 19 13:28:55 2009 +0100
     4.3 @@ -125,8 +125,8 @@
     4.4  
     4.5      val (implicit, expr') = params_expr expr;
     4.6  
     4.7 -    val implicit' = map (#1 #> Binding.name_of) implicit;
     4.8 -    val fixed' = map (#1 #> Binding.name_of) fixed;
     4.9 +    val implicit' = map (#1 #> Name.of_binding) implicit;
    4.10 +    val fixed' = map (#1 #> Name.of_binding) fixed;
    4.11      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    4.12      val implicit'' =
    4.13        if strict then []
    4.14 @@ -352,7 +352,7 @@
    4.15      fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
    4.16        let
    4.17          val (parm_names, parm_types) = Locale.params_of thy loc |>
    4.18 -          map_split (fn (b, SOME T, _) => (Binding.name_of b, T))
    4.19 +          map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
    4.20              (*FIXME return value of Locale.params_of has strange type*)
    4.21          val inst' = prep_inst ctxt parm_names inst;
    4.22          val parm_types' = map (TypeInfer.paramify_vars o
    4.23 @@ -386,7 +386,7 @@
    4.24        prep_concl raw_concl (insts', elems, ctxt5);
    4.25  
    4.26      (* Retrieve parameter types *)
    4.27 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
    4.28 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)
    4.29        | _ => fn ps => ps) (Fixes fors :: elems') [];
    4.30      val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
    4.31      val parms = xs ~~ Ts;  (* params from expression and elements *)
     5.1 --- a/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:26:19 2009 +0100
     5.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:28:55 2009 +0100
     5.3 @@ -90,7 +90,7 @@
     5.4    let
     5.5      val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     5.6      val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
     5.7 -    val xs = map Binding.name_of bvars;
     5.8 +    val xs = map Name.of_binding bvars;
     5.9      val names = map2 Thm.def_binding_optional bvars bfacts;
    5.10      val eqs = mk_def ctxt (xs ~~ rhss);
    5.11      val lhss = map (fst o Logic.dest_equals) eqs;
     6.1 --- a/src/Pure/Isar/locale.ML	Thu Mar 19 13:26:19 2009 +0100
     6.2 +++ b/src/Pure/Isar/locale.ML	Thu Mar 19 13:28:55 2009 +0100
     6.3 @@ -181,7 +181,7 @@
     6.4  fun axioms_of thy = #axioms o the_locale thy;
     6.5  
     6.6  fun instance_of thy name morph = params_of thy name |>
     6.7 -  map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph);
     6.8 +  map ((fn (b, T, _) => Free (Name.of_binding b, the T)) #> Morphism.term morph);
     6.9  
    6.10  fun specification_of thy = #spec o the_locale thy;
    6.11  
     7.1 --- a/src/Pure/Isar/obtain.ML	Thu Mar 19 13:26:19 2009 +0100
     7.2 +++ b/src/Pure/Isar/obtain.ML	Thu Mar 19 13:28:55 2009 +0100
     7.3 @@ -119,7 +119,7 @@
     7.4      (*obtain vars*)
     7.5      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     7.6      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
     7.7 -    val xs = map (Binding.name_of o #1) vars;
     7.8 +    val xs = map (Name.of_binding o #1) vars;
     7.9  
    7.10      (*obtain asms*)
    7.11      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    7.12 @@ -258,7 +258,7 @@
    7.13  
    7.14  fun inferred_type (binding, _, mx) ctxt =
    7.15    let
    7.16 -    val x = Binding.name_of binding;
    7.17 +    val x = Name.of_binding binding;
    7.18      val (T, ctxt') = ProofContext.inferred_param x ctxt
    7.19    in ((x, T, mx), ctxt') end;
    7.20  
     8.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 19 13:26:19 2009 +0100
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 19 13:28:55 2009 +0100
     8.3 @@ -1003,7 +1003,7 @@
     8.4  fun prep_vars prep_typ internal =
     8.5    fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
     8.6      let
     8.7 -      val raw_x = Binding.name_of raw_b;
     8.8 +      val raw_x = Name.of_binding raw_b;
     8.9        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
    8.10        val _ = Syntax.is_identifier (no_skolem internal x) orelse
    8.11          error ("Illegal variable name: " ^ quote x);
    8.12 @@ -1113,7 +1113,7 @@
    8.13  fun gen_fixes prep raw_vars ctxt =
    8.14    let
    8.15      val (vars, _) = prep raw_vars ctxt;
    8.16 -    val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt;
    8.17 +    val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
    8.18      val ctxt'' =
    8.19        ctxt'
    8.20        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
     9.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 19 13:26:19 2009 +0100
     9.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 19 13:28:55 2009 +0100
     9.3 @@ -161,7 +161,7 @@
     9.4  fun gen_axioms do_print prep raw_vars raw_specs thy =
     9.5    let
     9.6      val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
     9.7 -    val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
     9.8 +    val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
     9.9  
    9.10      (*consts*)
    9.11      val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
    9.12 @@ -171,7 +171,7 @@
    9.13      val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
    9.14          fold_map Thm.add_axiom
    9.15            (map (apfst (fn a => Binding.map_name (K a) b))
    9.16 -            (PureThy.name_multi (Binding.name_of b) (map subst props)))
    9.17 +            (PureThy.name_multi (Name.of_binding b) (map subst props)))
    9.18          #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
    9.19  
    9.20      (*facts*)
    9.21 @@ -198,7 +198,7 @@
    9.22          [] => (Binding.name x, NoSyn)
    9.23        | [((b, _), mx)] =>
    9.24            let
    9.25 -            val y = Binding.name_of b;
    9.26 +            val y = Name.of_binding b;
    9.27              val _ = x = y orelse
    9.28                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
    9.29                  Position.str_of (Binding.pos_of b));
    9.30 @@ -234,7 +234,7 @@
    9.31          [] => (Binding.name x, NoSyn)
    9.32        | [((b, _), mx)] =>
    9.33            let
    9.34 -            val y = Binding.name_of b;
    9.35 +            val y = Name.of_binding b;
    9.36              val _ = x = y orelse
    9.37                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
    9.38                  Position.str_of (Binding.pos_of b));
    9.39 @@ -292,10 +292,10 @@
    9.40    | Element.Obtains obtains =>
    9.41        let
    9.42          val case_names = obtains |> map_index (fn (i, (b, _)) =>
    9.43 -          if Binding.is_empty b then string_of_int (i + 1) else Binding.name_of b);
    9.44 +          if Binding.is_empty b then string_of_int (i + 1) else Name.of_binding b);
    9.45          val constraints = obtains |> map (fn (_, (vars, _)) =>
    9.46            Element.Constrains
    9.47 -            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE)));
    9.48 +            (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE)));
    9.49  
    9.50          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    9.51          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
    9.52 @@ -305,7 +305,7 @@
    9.53          fun assume_case ((name, (vars, _)), asms) ctxt' =
    9.54            let
    9.55              val bs = map fst vars;
    9.56 -            val xs = map Binding.name_of bs;
    9.57 +            val xs = map Name.of_binding bs;
    9.58              val props = map fst asms;
    9.59              val (Ts, _) = ctxt'
    9.60                |> fold Variable.declare_term props
    10.1 --- a/src/Pure/sign.ML	Thu Mar 19 13:26:19 2009 +0100
    10.2 +++ b/src/Pure/sign.ML	Thu Mar 19 13:28:55 2009 +0100
    10.3 @@ -434,7 +434,7 @@
    10.4  
    10.5  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    10.6    let
    10.7 -    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Binding.name_of a, n, mx)) types) syn;
    10.8 +    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
    10.9      val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
   10.10      val tags = [(Markup.theory_nameN, Context.theory_name thy)];
   10.11      val tsig' = fold (Type.add_type naming tags) decls tsig;
   10.12 @@ -445,7 +445,7 @@
   10.13  
   10.14  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   10.15    let
   10.16 -    val syn' = Syntax.update_consts (map Binding.name_of ns) syn;
   10.17 +    val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
   10.18      val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
   10.19    in (naming, syn', tsig', consts) end);
   10.20  
   10.21 @@ -456,7 +456,7 @@
   10.22    thy |> map_sign (fn (naming, syn, tsig, consts) =>
   10.23      let
   10.24        val ctxt = ProofContext.init thy;
   10.25 -      val syn' = Syntax.update_type_gram [(Binding.name_of a, length vs, mx)] syn;
   10.26 +      val syn' = Syntax.update_type_gram [(Name.of_binding a, length vs, mx)] syn;
   10.27        val b = Binding.map_name (Syntax.type_name mx) a;
   10.28        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
   10.29          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   10.30 @@ -504,10 +504,10 @@
   10.31      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
   10.32      fun prep (raw_b, raw_T, raw_mx) =
   10.33        let
   10.34 -        val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
   10.35 +        val (mx_name, mx) = Syntax.const_mixfix (Name.of_binding raw_b) raw_mx;
   10.36          val b = Binding.map_name (K mx_name) raw_b;
   10.37          val c = full_name thy b;
   10.38 -        val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
   10.39 +        val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
   10.40          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
   10.41            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
   10.42          val T' = Logic.varifyT T;
   10.43 @@ -568,7 +568,7 @@
   10.44  fun primitive_class (bclass, classes) thy =
   10.45    thy |> map_sign (fn (naming, syn, tsig, consts) =>
   10.46      let
   10.47 -      val syn' = Syntax.update_consts [Binding.name_of bclass] syn;
   10.48 +      val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
   10.49        val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
   10.50      in (naming, syn', tsig', consts) end)
   10.51    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];