explicit type Name.binding for higher-specification elements;
authorwenzelm
Tue Sep 02 14:10:45 2008 +0200 (2008-09-02)
changeset 28083103d9282a946
parent 28082 37350f301128
child 28084 a05ca48ef263
explicit type Name.binding for higher-specification elements;
src/HOL/Library/Eval.thy
src/HOL/Library/RType.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Typedef.thy
src/HOL/ex/Quickcheck.thy
src/HOLCF/Tools/fixrec_package.ML
src/HOLCF/Tools/pcpodef_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/class.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/theory_target.ML
src/Pure/Tools/invoke.ML
src/Pure/axclass.ML
src/Tools/induct.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4        thy
     1.5        |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
     1.6        |> `(fn lthy => Syntax.check_term lthy eq)
     1.7 -      |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
     1.8 +      |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
     1.9        |> snd
    1.10        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.11        |> LocalTheory.exit
     2.1 --- a/src/HOL/Library/RType.thy	Tue Sep 02 14:10:32 2008 +0200
     2.2 +++ b/src/HOL/Library/RType.thy	Tue Sep 02 14:10:45 2008 +0200
     2.3 @@ -67,7 +67,7 @@
     2.4      thy
     2.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort rtype})
     2.6      |> `(fn lthy => Syntax.check_term lthy eq)
     2.7 -    |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
     2.8 +    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
     2.9      |> snd
    2.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    2.11      |> LocalTheory.exit
     3.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Sep 02 14:10:32 2008 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Sep 02 14:10:45 2008 +0200
     3.3 @@ -265,9 +265,9 @@
     3.4                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
     3.5        in
     3.6            AxClass.define_class (cl_name, ["HOL.type"]) []
     3.7 -                [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
     3.8 -                 ((cl_name ^ "2", []), [axiom2]),                           
     3.9 -                 ((cl_name ^ "3", []), [axiom3])] thy                          
    3.10 +                [((Name.binding (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    3.11 +                 ((Name.binding (cl_name ^ "2"), []), [axiom2]),                           
    3.12 +                 ((Name.binding (cl_name ^ "3"), []), [axiom3])] thy
    3.13        end) ak_names_types thy6;
    3.14  
    3.15      (* proves that every pt_<ak>-type together with <ak>-type *)
    3.16 @@ -313,7 +313,7 @@
    3.17            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    3.18  
    3.19         in  
    3.20 -        AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    3.21 +        AxClass.define_class (cl_name, [pt_name]) [] [((Name.binding (cl_name ^ "1"), []), [axiom1])] thy            
    3.22         end) ak_names_types thy8; 
    3.23           
    3.24       (* proves that every fs_<ak>-type together with <ak>-type   *)
    3.25 @@ -362,7 +362,8 @@
    3.26                             (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    3.27                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    3.28                 in  
    3.29 -                 AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
    3.30 +                 AxClass.define_class (cl_name, ["HOL.type"]) []
    3.31 +                   [((Name.binding (cl_name ^ "1"), []), [ax1])] thy'  
    3.32                 end) ak_names_types thy) ak_names_types thy12;
    3.33  
    3.34          (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
     4.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Sep 02 14:10:32 2008 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Sep 02 14:10:45 2008 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  structure NominalInduct:
     4.6  sig
     4.7 -  val nominal_induct_tac: Proof.context -> (string option * term) option list list ->
     4.8 +  val nominal_induct_tac: Proof.context -> (Name.binding option * term) option list list ->
     4.9      (string * typ) list -> (string * typ) list list -> thm list ->
    4.10      thm list -> int -> RuleCases.cases_tactic
    4.11    val nominal_induct_method: Method.src -> Proof.context -> Method.method
    4.12 @@ -31,7 +31,6 @@
    4.13  
    4.14  fun inst_mutual_rule ctxt insts avoiding rules =
    4.15    let
    4.16 -
    4.17      val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
    4.18      val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
    4.19      val (cases, consumes) = RuleCases.get joined_rule;
    4.20 @@ -132,7 +131,7 @@
    4.21  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
    4.22  
    4.23  val def_inst =
    4.24 -  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
    4.25 +  ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
    4.26        -- Args.term) >> SOME ||
    4.27      inst >> Option.map (pair NONE);
    4.28  
     5.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Sep 02 14:10:32 2008 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Sep 02 14:10:45 2008 +0200
     5.3 @@ -286,7 +286,7 @@
     5.4                else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
     5.5              end;
     5.6          in
     5.7 -          (("", []), HOLogic.mk_Trueprop (HOLogic.mk_eq
     5.8 +          ((Name.no_binding, []), HOLogic.mk_Trueprop (HOLogic.mk_eq
     5.9              (Free (nth perm_names_types' i) $
    5.10                 Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
    5.11                 list_comb (c, args),
    5.12 @@ -298,7 +298,7 @@
    5.13        PrimrecPackage.add_primrec_overloaded
    5.14          (map (fn (s, sT) => (s, sT, false))
    5.15             (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
    5.16 -        (map (fn s => (s, NONE, NoSyn)) perm_names') perm_eqs thy1;
    5.17 +        (map (fn s => (Name.binding s, NONE, NoSyn)) perm_names') perm_eqs thy1;
    5.18  
    5.19      (**** prove that permutation functions introduced by unfolding are ****)
    5.20      (**** equivalent to already existing permutation functions         ****)
    5.21 @@ -559,11 +559,11 @@
    5.22      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
    5.23          InductivePackage.add_inductive_global (serial_string ())
    5.24            {quiet_mode = false, verbose = false, kind = Thm.internalK,
    5.25 -           alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false,
    5.26 +           alt_name = Name.binding big_rep_name, coind = false, no_elim = true, no_ind = false,
    5.27             skip_mono = true}
    5.28 -          (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
    5.29 +          (map (fn (s, T) => ((Name.binding s, T --> HOLogic.boolT), NoSyn))
    5.30               (rep_set_names' ~~ recTs'))
    5.31 -          [] (map (fn x => (("", []), x)) intr_ts) [] thy3;
    5.32 +          [] (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy3;
    5.33  
    5.34      (**** Prove that representing set is closed under permutation ****)
    5.35  
    5.36 @@ -1476,11 +1476,11 @@
    5.37        thy10 |>
    5.38          InductivePackage.add_inductive_global (serial_string ())
    5.39            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    5.40 -           alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false,
    5.41 +           alt_name = Name.binding big_rec_name, coind = false, no_elim = false, no_ind = false,
    5.42             skip_mono = true}
    5.43 -          (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    5.44 +          (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    5.45            (map dest_Free rec_fns)
    5.46 -          (map (fn x => (("", []), x)) rec_intr_ts) [] ||>
    5.47 +          (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] ||>
    5.48        PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
    5.49  
    5.50      (** equivariance **)
     6.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 02 14:10:32 2008 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 02 14:10:45 2008 +0200
     6.3 @@ -9,13 +9,13 @@
     6.4  signature NOMINAL_PRIMREC =
     6.5  sig
     6.6    val add_primrec: string -> string list option -> string option ->
     6.7 -    ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
     6.8 +    ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
     6.9    val add_primrec_unchecked: string -> string list option -> string option ->
    6.10 -    ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
    6.11 +    ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
    6.12    val add_primrec_i: string -> term list option -> term option ->
    6.13 -    ((bstring * term) * attribute list) list -> theory -> Proof.state
    6.14 +    ((Name.binding * term) * attribute list) list -> theory -> Proof.state
    6.15    val add_primrec_unchecked_i: string -> term list option -> term option ->
    6.16 -    ((bstring * term) * attribute list) list -> theory -> Proof.state
    6.17 +    ((Name.binding * term) * attribute list) list -> theory -> Proof.state
    6.18  end;
    6.19  
    6.20  structure NominalPrimrec : NOMINAL_PRIMREC =
    6.21 @@ -229,7 +229,8 @@
    6.22  
    6.23  fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
    6.24    let
    6.25 -    val (eqns, atts) = split_list eqns_atts;
    6.26 +    val (raw_eqns, atts) = split_list eqns_atts;
    6.27 +    val eqns = map (apfst Name.name_of) raw_eqns;
    6.28      val dt_info = NominalPackage.get_nominal_datatypes thy;
    6.29      val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
    6.30      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
     7.1 --- a/src/HOL/Statespace/state_space.ML	Tue Sep 02 14:10:32 2008 +0200
     7.2 +++ b/src/HOL/Statespace/state_space.ML	Tue Sep 02 14:10:45 2008 +0200
     7.3 @@ -61,7 +61,6 @@
     7.4      val update_tr' : Proof.context -> term list -> term
     7.5    end;
     7.6  
     7.7 -
     7.8  structure StateSpace: STATE_SPACE =
     7.9  struct
    7.10  
    7.11 @@ -303,7 +302,7 @@
    7.12  
    7.13      val attr = Attrib.internal type_attr;
    7.14  
    7.15 -    val assumes = Element.Assumes [((dist_thm_name,[attr]),
    7.16 +    val assumes = Element.Assumes [((Name.binding dist_thm_name,[attr]),
    7.17                      [(HOLogic.Trueprop $
    7.18                        (Const ("DistinctTreeProver.all_distinct",
    7.19                                   Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
    7.20 @@ -445,7 +444,7 @@
    7.21           NONE => []
    7.22         | SOME s =>
    7.23            let
    7.24 -	    val fx = Element.Fixes [(s,SOME (string_of_typ stateT),NoSyn)];
    7.25 +	    val fx = Element.Fixes [(Name.binding s,SOME (string_of_typ stateT),NoSyn)];
    7.26              val cs = Element.Constrains
    7.27                         (map (fn (n,T) =>  (n,string_of_typ T))
    7.28                           ((map (fn (n,_) => (n,nameT)) all_comps) @
     8.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 02 14:10:32 2008 +0200
     8.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 02 14:10:45 2008 +0200
     8.3 @@ -156,11 +156,11 @@
     8.4      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     8.5          InductivePackage.add_inductive_global (serial_string ())
     8.6            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
     8.7 -            alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true,
     8.8 +            alt_name = Name.binding big_rec_name', coind = false, no_elim = false, no_ind = true,
     8.9              skip_mono = true}
    8.10 -          (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    8.11 +          (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    8.12            (map dest_Free rec_fns)
    8.13 -          (map (fn x => (("", []), x)) rec_intr_ts) [] thy0;
    8.14 +          (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] thy0;
    8.15  
    8.16      (* prove uniqueness and termination of primrec combinators *)
    8.17  
     9.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 02 14:10:32 2008 +0200
     9.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 02 14:10:45 2008 +0200
     9.3 @@ -442,7 +442,7 @@
     9.4            (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
     9.5          val def' = Syntax.check_term lthy def;
     9.6          val ((_, (_, thm)), lthy') = Specification.definition
     9.7 -          (NONE, (("", []), def')) lthy;
     9.8 +          (NONE, ((Name.no_binding, []), def')) lthy;
     9.9          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
    9.10          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
    9.11        in (thm', lthy') end;
    10.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 02 14:10:32 2008 +0200
    10.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 02 14:10:45 2008 +0200
    10.3 @@ -184,10 +184,10 @@
    10.4      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
    10.5          InductivePackage.add_inductive_global (serial_string ())
    10.6            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    10.7 -           alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false,
    10.8 +           alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
    10.9             skip_mono = true}
   10.10 -          (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
   10.11 -          (map (fn x => (("", []), x)) intr_ts) [] thy1;
   10.12 +          (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
   10.13 +          (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy1;
   10.14  
   10.15      (********************************* typedef ********************************)
   10.16  
    11.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Sep 02 14:10:32 2008 +0200
    11.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Sep 02 14:10:45 2008 +0200
    11.3 @@ -66,7 +66,7 @@
    11.4                                        psimps, pinducts, termination, defname}) phi =
    11.5      let
    11.6        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    11.7 -      val name = Morphism.name phi
    11.8 +      val name = Name.name_of o Morphism.name phi o Name.binding
    11.9      in
   11.10        FundefCtxData { add_simps = add_simps, case_names = case_names,
   11.11                        fs = map term fs, R = term R, psimps = fact psimps, 
    12.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Tue Sep 02 14:10:32 2008 +0200
    12.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Tue Sep 02 14:10:45 2008 +0200
    12.3 @@ -10,8 +10,8 @@
    12.4  sig
    12.5      val prepare_fundef : FundefCommon.fundef_config
    12.6                           -> string (* defname *)
    12.7 -                         -> ((string * typ) * mixfix) list (* defined symbol *)
    12.8 -                         -> ((string * typ) list * term list * term * term) list (* specification *)
    12.9 +                         -> ((bstring * typ) * mixfix) list (* defined symbol *)
   12.10 +                         -> ((bstring * typ) list * term list * term * term) list (* specification *)
   12.11                           -> local_theory
   12.12  
   12.13                           -> (term   (* f *)
   12.14 @@ -31,22 +31,22 @@
   12.15  open FundefCommon
   12.16  
   12.17  datatype globals =
   12.18 -   Globals of { 
   12.19 -         fvar: term, 
   12.20 -         domT: typ, 
   12.21 +   Globals of {
   12.22 +         fvar: term,
   12.23 +         domT: typ,
   12.24           ranT: typ,
   12.25 -         h: term, 
   12.26 -         y: term, 
   12.27 -         x: term, 
   12.28 -         z: term, 
   12.29 -         a: term, 
   12.30 -         P: term, 
   12.31 -         D: term, 
   12.32 +         h: term,
   12.33 +         y: term,
   12.34 +         x: term,
   12.35 +         z: term,
   12.36 +         a: term,
   12.37 +         P: term,
   12.38 +         D: term,
   12.39           Pbool:term
   12.40  }
   12.41  
   12.42  
   12.43 -datatype rec_call_info = 
   12.44 +datatype rec_call_info =
   12.45    RCInfo of
   12.46    {
   12.47     RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
   12.48 @@ -55,7 +55,7 @@
   12.49  
   12.50     llRI: thm,
   12.51     h_assum: term
   12.52 -  } 
   12.53 +  }
   12.54  
   12.55  
   12.56  datatype clause_context =
   12.57 @@ -69,7 +69,7 @@
   12.58      rhs: term,
   12.59  
   12.60      cqs: cterm list,
   12.61 -    ags: thm list,     
   12.62 +    ags: thm list,
   12.63      case_hyp : thm
   12.64    }
   12.65  
   12.66 @@ -80,7 +80,7 @@
   12.67  
   12.68  
   12.69  datatype clause_info =
   12.70 -  ClauseInfo of 
   12.71 +  ClauseInfo of
   12.72       {
   12.73        no: int,
   12.74        qglr : ((string * typ) list * term list * term * term),
   12.75 @@ -166,16 +166,16 @@
   12.76        val gs = map inst pre_gs
   12.77        val lhs = inst pre_lhs
   12.78        val rhs = inst pre_rhs
   12.79 -                
   12.80 +
   12.81        val cqs = map (cterm_of thy) qs
   12.82        val ags = map (assume o cterm_of thy) gs
   12.83 -                  
   12.84 +
   12.85        val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   12.86      in
   12.87 -      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, 
   12.88 +      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
   12.89                        cqs = cqs, ags = ags, case_hyp = case_hyp }
   12.90      end
   12.91 -      
   12.92 +
   12.93  
   12.94  (* lowlevel term function *)
   12.95  fun abstract_over_list vs body =
   12.96 @@ -188,7 +188,7 @@
   12.97            Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
   12.98          | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
   12.99          | _ => raise SAME);
  12.100 -  in 
  12.101 +  in
  12.102      fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
  12.103    end
  12.104  
  12.105 @@ -233,7 +233,7 @@
  12.106               cdata=cdata,
  12.107               qglr=qglr,
  12.108  
  12.109 -             lGI=lGI, 
  12.110 +             lGI=lGI,
  12.111               RCs=RC_infos,
  12.112               tree=tree
  12.113              }
  12.114 @@ -260,11 +260,11 @@
  12.115  
  12.116  (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
  12.117  (* if j < i, then turn around *)
  12.118 -fun get_compat_thm thy cts i j ctxi ctxj = 
  12.119 +fun get_compat_thm thy cts i j ctxi ctxj =
  12.120      let
  12.121        val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
  12.122        val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
  12.123 -          
  12.124 +
  12.125        val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
  12.126      in if j < i then
  12.127           let
  12.128 @@ -324,14 +324,14 @@
  12.129          val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
  12.130          val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
  12.131  
  12.132 -        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} 
  12.133 +        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
  12.134              = mk_clause_context x ctxti cdescj
  12.135  
  12.136          val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
  12.137          val compat = get_compat_thm thy compat_store i j cctxi cctxj
  12.138          val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
  12.139  
  12.140 -        val RLj_import = 
  12.141 +        val RLj_import =
  12.142              RLj |> fold forall_elim cqsj'
  12.143                  |> fold Thm.elim_implies agsj'
  12.144                  |> fold Thm.elim_implies Ghsj'
  12.145 @@ -426,7 +426,7 @@
  12.146          val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
  12.147  
  12.148          val _ = Output.debug (K "Proving cases for unique existence...")
  12.149 -        val (ex1s, values) = 
  12.150 +        val (ex1s, values) =
  12.151              split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
  12.152  
  12.153          val _ = Output.debug (K "Proving: Graph is a function")
  12.154 @@ -466,10 +466,10 @@
  12.155                        |> fold_rev (curry Logic.mk_implies) gs
  12.156                        |> fold_rev Logic.all (fvar :: qs)
  12.157            end
  12.158 -          
  12.159 +
  12.160        val G_intros = map2 mk_GIntro clauses RCss
  12.161 -                     
  12.162 -      val (GIntro_thms, (G, G_elim, G_induct, lthy)) = 
  12.163 +
  12.164 +      val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
  12.165            FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
  12.166      in
  12.167        ((G, GIntro_thms, G_elim, G_induct), lthy)
  12.168 @@ -479,13 +479,13 @@
  12.169  
  12.170  fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
  12.171      let
  12.172 -      val f_def = 
  12.173 +      val f_def =
  12.174            Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
  12.175                                  Abs ("y", ranT, G $ Bound 1 $ Bound 0))
  12.176                |> Syntax.check_term lthy
  12.177  
  12.178        val ((f, (_, f_defthm)), lthy) =
  12.179 -        LocalTheory.define Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
  12.180 +        LocalTheory.define Thm.internalK ((Name.binding (function_name fname), mixfix), ((Name.binding fdefname, []), f_def)) lthy
  12.181      in
  12.182        ((f, f_defthm), lthy)
  12.183      end
  12.184 @@ -507,7 +507,7 @@
  12.185  
  12.186        val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
  12.187  
  12.188 -      val (RIntro_thmss, (R, R_elim, _, lthy)) = 
  12.189 +      val (RIntro_thmss, (R, R_elim, _, lthy)) =
  12.190            fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
  12.191      in
  12.192        ((R, RIntro_thmss, R_elim), lthy)
  12.193 @@ -516,7 +516,7 @@
  12.194  
  12.195  fun fix_globals domT ranT fvar ctxt =
  12.196      let
  12.197 -      val ([h, y, x, z, a, D, P, Pbool],ctxt') = 
  12.198 +      val ([h, y, x, z, a, D, P, Pbool],ctxt') =
  12.199            Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
  12.200      in
  12.201        (Globals {h = Free (h, domT --> ranT),
  12.202 @@ -546,13 +546,13 @@
  12.203  
  12.204  
  12.205  (**********************************************************
  12.206 - *                   PROVING THE RULES 
  12.207 + *                   PROVING THE RULES
  12.208   **********************************************************)
  12.209  
  12.210  fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
  12.211      let
  12.212        val Globals {domT, z, ...} = globals
  12.213 -  
  12.214 +
  12.215        fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
  12.216            let
  12.217              val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
  12.218 @@ -563,7 +563,7 @@
  12.219                |> implies_intr z_smaller
  12.220                |> forall_intr (cterm_of thy z)
  12.221                |> (fn it => it COMP valthm)
  12.222 -              |> implies_intr lhs_acc 
  12.223 +              |> implies_intr lhs_acc
  12.224                |> asm_simplify (HOL_basic_ss addsimps [f_iff])
  12.225                |> fold_rev (implies_intr o cprop_of) ags
  12.226                |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  12.227 @@ -585,23 +585,23 @@
  12.228      let
  12.229        val Globals {domT, x, z, a, P, D, ...} = globals
  12.230        val acc_R = mk_acc domT R
  12.231 -                  
  12.232 +
  12.233        val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
  12.234        val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
  12.235 -                
  12.236 +
  12.237        val D_subset = cterm_of thy (Logic.all x
  12.238          (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
  12.239 -                     
  12.240 +
  12.241        val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
  12.242                      Logic.all x
  12.243                      (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
  12.244                                                      Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
  12.245                                                                        HOLogic.mk_Trueprop (D $ z)))))
  12.246                      |> cterm_of thy
  12.247 -                    
  12.248 -                    
  12.249 +
  12.250 +
  12.251    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
  12.252 -      val ihyp = Term.all domT $ Abs ("z", domT, 
  12.253 +      val ihyp = Term.all domT $ Abs ("z", domT,
  12.254                 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
  12.255                   HOLogic.mk_Trueprop (P $ Bound 0)))
  12.256             |> cterm_of thy
  12.257 @@ -610,36 +610,36 @@
  12.258  
  12.259    fun prove_case clause =
  12.260        let
  12.261 -    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, 
  12.262 +    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
  12.263                      qglr = (oqs, _, _, _), ...} = clause
  12.264 -                       
  12.265 +
  12.266      val case_hyp_conv = K (case_hyp RS eq_reflection)
  12.267 -    local open Conv in 
  12.268 +    local open Conv in
  12.269      val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
  12.270      val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
  12.271      end
  12.272 -          
  12.273 +
  12.274      fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
  12.275          sih |> forall_elim (cterm_of thy rcarg)
  12.276              |> Thm.elim_implies llRI
  12.277              |> fold_rev (implies_intr o cprop_of) CCas
  12.278              |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  12.279 -        
  12.280 +
  12.281      val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
  12.282 -                 
  12.283 +
  12.284      val step = HOLogic.mk_Trueprop (P $ lhs)
  12.285              |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
  12.286              |> fold_rev (curry Logic.mk_implies) gs
  12.287              |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
  12.288              |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  12.289              |> cterm_of thy
  12.290 -         
  12.291 +
  12.292      val P_lhs = assume step
  12.293             |> fold forall_elim cqs
  12.294 -           |> Thm.elim_implies lhs_D 
  12.295 +           |> Thm.elim_implies lhs_D
  12.296             |> fold Thm.elim_implies ags
  12.297             |> fold Thm.elim_implies P_recs
  12.298 -          
  12.299 +
  12.300      val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
  12.301             |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
  12.302             |> symmetric (* P lhs == P x *)
  12.303 @@ -650,17 +650,17 @@
  12.304        in
  12.305          (res, step)
  12.306        end
  12.307 -      
  12.308 +
  12.309    val (cases, steps) = split_list (map prove_case clauses)
  12.310 -                       
  12.311 +
  12.312    val istep = complete_thm
  12.313                  |> Thm.forall_elim_vars 0
  12.314                  |> fold (curry op COMP) cases (*  P x  *)
  12.315                  |> implies_intr ihyp
  12.316                  |> implies_intr (cprop_of x_D)
  12.317                  |> forall_intr (cterm_of thy x)
  12.318 -         
  12.319 -  val subset_induct_rule = 
  12.320 +
  12.321 +  val subset_induct_rule =
  12.322        acc_subset_induct
  12.323          |> (curry op COMP) (assume D_subset)
  12.324          |> (curry op COMP) (assume D_dcl)
  12.325 @@ -694,13 +694,13 @@
  12.326  (* FIXME: This should probably use fixed goals, to be more reliable and faster *)
  12.327  fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
  12.328      let
  12.329 -      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
  12.330 +      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
  12.331                        qglr = (oqs, _, _, _), ...} = clause
  12.332        val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
  12.333                            |> fold_rev (curry Logic.mk_implies) gs
  12.334                            |> cterm_of thy
  12.335      in
  12.336 -      Goal.init goal 
  12.337 +      Goal.init goal
  12.338        |> (SINGLE (resolve_tac [accI] 1)) |> the
  12.339        |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
  12.340        |> (SINGLE (CLASIMPSET auto_tac)) |> the
  12.341 @@ -721,26 +721,26 @@
  12.342        val Globals {x, z, ...} = globals
  12.343        val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
  12.344                        qglr=(oqs, _, _, _), ...} = clause
  12.345 -          
  12.346 +
  12.347        val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
  12.348 -                    
  12.349 -      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
  12.350 +
  12.351 +      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
  12.352            let
  12.353              val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub)
  12.354 -                       
  12.355 +
  12.356              val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
  12.357                        |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
  12.358 -                      |> FundefCtxTree.export_term (fixes, assumes) 
  12.359 +                      |> FundefCtxTree.export_term (fixes, assumes)
  12.360                        |> fold_rev (curry Logic.mk_implies o prop_of) ags
  12.361                        |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  12.362                        |> cterm_of thy
  12.363 -                      
  12.364 +
  12.365              val thm = assume hyp
  12.366                        |> fold forall_elim cqs
  12.367                        |> fold Thm.elim_implies ags
  12.368                        |> FundefCtxTree.import_thm thy (fixes, assumes)
  12.369                        |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
  12.370 -                      
  12.371 +
  12.372              val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
  12.373  
  12.374              val acc = thm COMP ih_case
  12.375 @@ -748,7 +748,7 @@
  12.376              |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
  12.377  
  12.378              val ethm = z_acc_local
  12.379 -                         |> FundefCtxTree.export_thm thy (fixes, 
  12.380 +                         |> FundefCtxTree.export_thm thy (fixes,
  12.381                                                            z_eq_arg :: case_hyp :: ags @ assumes)
  12.382                           |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  12.383  
  12.384 @@ -766,24 +766,24 @@
  12.385      let
  12.386        val Globals { domT, x, z, ... } = globals
  12.387        val acc_R = mk_acc domT R
  12.388 -                  
  12.389 +
  12.390        val R' = Free ("R", fastype_of R)
  12.391 -               
  12.392 +
  12.393        val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
  12.394        val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
  12.395 -                    
  12.396 +
  12.397        val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
  12.398 -                          
  12.399 +
  12.400        (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
  12.401 -      val ihyp = Term.all domT $ Abs ("z", domT, 
  12.402 +      val ihyp = Term.all domT $ Abs ("z", domT,
  12.403                                   Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
  12.404                                     HOLogic.mk_Trueprop (acc_R $ Bound 0)))
  12.405                       |> cterm_of thy
  12.406  
  12.407        val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
  12.408 -                   
  12.409 -      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) 
  12.410 -                  
  12.411 +
  12.412 +      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
  12.413 +
  12.414        val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
  12.415      in
  12.416        R_cases
  12.417 @@ -809,7 +809,7 @@
  12.418          |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
  12.419          |> forall_intr (cterm_of thy Rrel)
  12.420      end
  12.421 -    
  12.422 +
  12.423  
  12.424  
  12.425  (* Tail recursion (probably very fragile)
  12.426 @@ -828,7 +828,7 @@
  12.427        val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
  12.428            Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
  12.429                       (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
  12.430 -                     (fn {prems=[a], ...} => 
  12.431 +                     (fn {prems=[a], ...} =>
  12.432                           ((rtac (G_induct OF [a]))
  12.433                              THEN_ALL_NEW (rtac accI)
  12.434                              THEN_ALL_NEW (etac R_cases)
  12.435 @@ -841,13 +841,13 @@
  12.436              val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
  12.437              val thy = ProofContext.theory_of ctxt
  12.438              val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  12.439 -                        
  12.440 +
  12.441              val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
  12.442              val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
  12.443              fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
  12.444            in
  12.445              Goal.prove ctxt [] [] trsimp
  12.446 -                       (fn _ =>  
  12.447 +                       (fn _ =>
  12.448                             rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
  12.449                                  THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
  12.450                                  THEN (SIMPSET' simp_default_tac 1)
  12.451 @@ -862,12 +862,12 @@
  12.452  
  12.453  fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
  12.454      let
  12.455 -      val FundefConfig {domintros, tailrec, default=default_str, ...} = config 
  12.456 -                                                         
  12.457 +      val FundefConfig {domintros, tailrec, default=default_str, ...} = config
  12.458 +
  12.459        val fvar = Free (fname, fT)
  12.460        val domT = domain_type fT
  12.461        val ranT = range_type fT
  12.462 -                            
  12.463 +
  12.464        val default = Syntax.parse_term lthy default_str
  12.465          |> TypeInfer.constrain fT |> Syntax.check_term lthy
  12.466  
  12.467 @@ -875,30 +875,30 @@
  12.468  
  12.469        val Globals { x, h, ... } = globals
  12.470  
  12.471 -      val clauses = map (mk_clause_context x ctxt') abstract_qglrs 
  12.472 +      val clauses = map (mk_clause_context x ctxt') abstract_qglrs
  12.473  
  12.474        val n = length abstract_qglrs
  12.475  
  12.476 -      fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
  12.477 +      fun build_tree (ClauseContext { ctxt, rhs, ...}) =
  12.478              FundefCtxTree.mk_tree (fname, fT) h ctxt rhs
  12.479  
  12.480        val trees = map build_tree clauses
  12.481        val RCss = map find_calls trees
  12.482  
  12.483 -      val ((G, GIntro_thms, G_elim, G_induct), lthy) = 
  12.484 +      val ((G, GIntro_thms, G_elim, G_induct), lthy) =
  12.485            PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
  12.486  
  12.487 -      val ((f, f_defthm), lthy) = 
  12.488 +      val ((f, f_defthm), lthy) =
  12.489            PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
  12.490  
  12.491        val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
  12.492        val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
  12.493  
  12.494 -      val ((R, RIntro_thmss, R_elim), lthy) = 
  12.495 +      val ((R, RIntro_thmss, R_elim), lthy) =
  12.496            PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
  12.497  
  12.498 -      val (_, lthy) = 
  12.499 -          LocalTheory.abbrev Syntax.mode_default ((dom_name defname, NoSyn), mk_acc domT R) lthy
  12.500 +      val (_, lthy) =
  12.501 +          LocalTheory.abbrev Syntax.mode_default ((Name.binding (dom_name defname), NoSyn), mk_acc domT R) lthy
  12.502  
  12.503        val newthy = ProofContext.theory_of lthy
  12.504        val clauses = map (transfer_clause_ctx newthy) clauses
  12.505 @@ -918,31 +918,31 @@
  12.506  
  12.507        fun mk_partial_rules provedgoal =
  12.508            let
  12.509 -            val newthy = theory_of_thm provedgoal (*FIXME*) 
  12.510 +            val newthy = theory_of_thm provedgoal (*FIXME*)
  12.511  
  12.512 -            val (graph_is_function, complete_thm) = 
  12.513 +            val (graph_is_function, complete_thm) =
  12.514                  provedgoal
  12.515                    |> Conjunction.elim
  12.516                    |> apfst (Thm.forall_elim_vars 0)
  12.517 -                
  12.518 +
  12.519              val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
  12.520 -                        
  12.521 +
  12.522              val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
  12.523 -                         
  12.524 -            val simple_pinduct = PROFILE "Proving partial induction rule" 
  12.525 +
  12.526 +            val simple_pinduct = PROFILE "Proving partial induction rule"
  12.527                                                             (mk_partial_induct_rule newthy globals R complete_thm) xclauses
  12.528 -                                                   
  12.529 -                                                   
  12.530 +
  12.531 +
  12.532              val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
  12.533 -                              
  12.534 -            val dom_intros = if domintros 
  12.535 +
  12.536 +            val dom_intros = if domintros
  12.537                               then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
  12.538                               else NONE
  12.539              val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
  12.540 -                                                                        
  12.541 -          in 
  12.542 -            FundefResult {fs=[f], G=G, R=R, cases=complete_thm, 
  12.543 -                          psimps=psimps, simple_pinducts=[simple_pinduct], 
  12.544 +
  12.545 +          in
  12.546 +            FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
  12.547 +                          psimps=psimps, simple_pinducts=[simple_pinduct],
  12.548                            termination=total_intro, trsimps=trsimps,
  12.549                            domintros=dom_intros}
  12.550            end
  12.551 @@ -951,6 +951,4 @@
  12.552      end
  12.553  
  12.554  
  12.555 -
  12.556 -
  12.557  end
    13.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Sep 02 14:10:32 2008 +0200
    13.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Sep 02 14:10:45 2008 +0200
    13.3 @@ -56,7 +56,7 @@
    13.4  fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
    13.5      let
    13.6        val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
    13.7 -      val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
    13.8 +      val (_, ctx') = ProofContext.add_fixes_i [(Name.binding n', SOME T, NoSyn)] ctx
    13.9  
   13.10        val (n'', body) = Term.dest_abs (n', T, b) 
   13.11        val _ = (n' = n'') orelse error "dest_all_ctx"
    14.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 02 14:10:32 2008 +0200
    14.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 02 14:10:45 2008 +0200
    14.3 @@ -9,15 +9,15 @@
    14.4  
    14.5  signature FUNDEF_PACKAGE =
    14.6  sig
    14.7 -    val add_fundef :  (string * string option * mixfix) list
    14.8 -                      -> ((bstring * Attrib.src list) * string) list 
    14.9 +    val add_fundef :  (Name.binding * string option * mixfix) list
   14.10 +                      -> ((Name.binding * Attrib.src list) * string) list 
   14.11                        -> FundefCommon.fundef_config
   14.12                        -> bool list
   14.13                        -> local_theory
   14.14                        -> Proof.state
   14.15  
   14.16 -    val add_fundef_i:  (string * typ option * mixfix) list
   14.17 -                       -> ((bstring * Attrib.src list) * term) list
   14.18 +    val add_fundef_i:  (Name.binding * typ option * mixfix) list
   14.19 +                       -> ((Name.binding * Attrib.src list) * term) list
   14.20                         -> FundefCommon.fundef_config
   14.21                         -> bool list
   14.22                         -> local_theory
   14.23 @@ -36,7 +36,7 @@
   14.24  open FundefLib
   14.25  open FundefCommon
   14.26  
   14.27 -val note_theorem = LocalTheory.note Thm.theoremK
   14.28 +fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Name.binding name, atts), ths)
   14.29  
   14.30  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
   14.31  
   14.32 @@ -95,7 +95,9 @@
   14.33  
   14.34  fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
   14.35      let
   14.36 -      val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
   14.37 +      val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
   14.38 +      val fixes = map (apfst (apfst Name.name_of)) fixes0;
   14.39 +      val spec = map (apfst (apfst Name.name_of)) spec0;
   14.40        val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
   14.41  
   14.42        val defname = mk_defname fixes
   14.43 @@ -145,10 +147,10 @@
   14.44          val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
   14.45      in
   14.46        lthy
   14.47 -        |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd
   14.48 -        |> ProofContext.note_thmss_i "" [(("", [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
   14.49 +        |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.rule_del]), [([allI], [])])] |> snd
   14.50 +        |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
   14.51          |> ProofContext.note_thmss_i ""
   14.52 -          [(("termination", [ContextRules.intro_bang (SOME 0)]),
   14.53 +          [((Name.binding "termination", [ContextRules.intro_bang (SOME 0)]),
   14.54              [([Goal.norm_result termination], [])])] |> snd
   14.55          |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
   14.56      end
    15.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Sep 02 14:10:32 2008 +0200
    15.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Sep 02 14:10:45 2008 +0200
    15.3 @@ -14,7 +14,7 @@
    15.4                         -> thm list * (term * thm * thm * local_theory)
    15.5  end
    15.6  
    15.7 -structure FundefInductiveWrap =
    15.8 +structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP =
    15.9  struct
   15.10  
   15.11  open FundefLib
   15.12 @@ -44,14 +44,14 @@
   15.13              {quiet_mode = false,
   15.14                verbose = ! Toplevel.debug,
   15.15                kind = Thm.internalK,
   15.16 -              alt_name = "",
   15.17 +              alt_name = Name.no_binding,
   15.18                coind = false,
   15.19                no_elim = false,
   15.20                no_ind = false,
   15.21                skip_mono = true}
   15.22 -            [((R, T), NoSyn)] (* the relation *)
   15.23 +            [((Name.binding R, T), NoSyn)] (* the relation *)
   15.24              [] (* no parameters *)
   15.25 -            (map (fn t => (("", []), t)) defs) (* the intros *)
   15.26 +            (map (fn t => ((Name.no_binding, []), t)) defs) (* the intros *)
   15.27              [] (* no special monos *)
   15.28              lthy
   15.29  
    16.1 --- a/src/HOL/Tools/function_package/mutual.ML	Tue Sep 02 14:10:32 2008 +0200
    16.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Tue Sep 02 14:10:45 2008 +0200
    16.3 @@ -150,8 +150,8 @@
    16.4        fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
    16.5            let
    16.6              val ((f, (_, f_defthm)), lthy') =
    16.7 -              LocalTheory.define Thm.internalK ((fname, mixfix),
    16.8 -                                            ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
    16.9 +              LocalTheory.define Thm.internalK ((Name.binding fname, mixfix),
   16.10 +                                            ((Name.binding (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
   16.11                                lthy
   16.12            in
   16.13              (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
    17.1 --- a/src/HOL/Tools/function_package/size.ML	Tue Sep 02 14:10:32 2008 +0200
    17.2 +++ b/src/HOL/Tools/function_package/size.ML	Tue Sep 02 14:10:45 2008 +0200
    17.3 @@ -132,8 +132,8 @@
    17.4      fun define_overloaded (def_name, eq) lthy =
    17.5        let
    17.6          val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
    17.7 -        val ((_, (_, thm)), lthy') = lthy
    17.8 -          |> LocalTheory.define Thm.definitionK ((c, NoSyn), ((def_name, []), rhs));
    17.9 +        val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
   17.10 +          ((Name.binding c, NoSyn), ((Name.binding def_name, []), rhs));
   17.11          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
   17.12          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   17.13        in (thm', lthy') end;
    18.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Sep 02 14:10:32 2008 +0200
    18.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Sep 02 14:10:45 2008 +0200
    18.3 @@ -33,22 +33,25 @@
    18.4    val inductive_forall_name: string
    18.5    val inductive_forall_def: thm
    18.6    val rulify: thm -> thm
    18.7 -  val inductive_cases: ((bstring * Attrib.src list) * string list) list ->
    18.8 +  val inductive_cases: ((Name.binding * Attrib.src list) * string list) list ->
    18.9      Proof.context -> thm list list * local_theory
   18.10 -  val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
   18.11 +  val inductive_cases_i: ((Name.binding * Attrib.src list) * term list) list ->
   18.12      Proof.context -> thm list list * local_theory
   18.13    type inductive_flags
   18.14    val add_inductive_i:
   18.15 -    inductive_flags -> ((string * typ) * mixfix) list ->
   18.16 -    (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
   18.17 +    inductive_flags -> ((Name.binding * typ) * mixfix) list ->
   18.18 +    (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
   18.19        local_theory -> inductive_result * local_theory
   18.20 -  val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
   18.21 -    (string * string option * mixfix) list ->
   18.22 -    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
   18.23 +  val add_inductive: bool -> bool ->
   18.24 +    (Name.binding * string option * mixfix) list ->
   18.25 +    (Name.binding * string option * mixfix) list ->
   18.26 +    ((Name.binding * Attrib.src list) * string) list ->
   18.27 +    (Facts.ref * Attrib.src list) list ->
   18.28      local_theory -> inductive_result * local_theory
   18.29    val add_inductive_global: string -> inductive_flags ->
   18.30 -    ((string * typ) * mixfix) list -> (string * typ) list ->
   18.31 -    ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
   18.32 +    ((Name.binding * typ) * mixfix) list ->
   18.33 +    (string * typ) list ->
   18.34 +    ((Name.binding * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
   18.35    val arities_of: thm -> (string * int) list
   18.36    val params_of: thm -> term list
   18.37    val partition_rules: thm -> thm list -> (string * thm list) list
   18.38 @@ -62,18 +65,19 @@
   18.39  sig
   18.40    include BASIC_INDUCTIVE_PACKAGE
   18.41    type add_ind_def
   18.42 -  val declare_rules: string -> bstring -> bool -> bool -> string list ->
   18.43 -    thm list -> bstring list -> Attrib.src list list -> (thm * string list) list ->
   18.44 +  val declare_rules: string -> Name.binding -> bool -> bool -> string list ->
   18.45 +    thm list -> Name.binding list -> Attrib.src list list -> (thm * string list) list ->
   18.46      thm -> local_theory -> thm list * thm list * thm * local_theory
   18.47    val add_ind_def: add_ind_def
   18.48 -  val gen_add_inductive_i: add_ind_def ->
   18.49 -    inductive_flags -> ((string * typ) * mixfix) list ->
   18.50 -    (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
   18.51 -      local_theory -> inductive_result * local_theory
   18.52 -  val gen_add_inductive: add_ind_def ->
   18.53 -    bool -> bool -> (string * string option * mixfix) list ->
   18.54 -    (string * string option * mixfix) list ->
   18.55 -    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
   18.56 +  val gen_add_inductive_i: add_ind_def -> inductive_flags ->
   18.57 +    ((Name.binding * typ) * mixfix) list ->
   18.58 +    (string * typ) list ->
   18.59 +    ((Name.binding * Attrib.src list) * term) list -> thm list ->
   18.60 +    local_theory -> inductive_result * local_theory
   18.61 +  val gen_add_inductive: add_ind_def -> bool -> bool ->
   18.62 +    (Name.binding * string option * mixfix) list ->
   18.63 +    (Name.binding * string option * mixfix) list ->
   18.64 +    ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
   18.65      local_theory -> inductive_result * local_theory
   18.66    val gen_ind_decl: add_ind_def -> bool ->
   18.67      OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
   18.68 @@ -258,8 +262,9 @@
   18.69  
   18.70  in
   18.71  
   18.72 -fun check_rule ctxt cs params ((name, att), rule) =
   18.73 +fun check_rule ctxt cs params ((binding, att), rule) =
   18.74    let
   18.75 +    val name = Name.name_of binding;
   18.76      val params' = Term.variant_frees rule (Logic.strip_params rule);
   18.77      val frees = rev (map Free params');
   18.78      val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
   18.79 @@ -294,7 +299,7 @@
   18.80              List.app check_prem (prems ~~ aprems))
   18.81           else err_in_rule ctxt name rule' bad_concl
   18.82       | _ => err_in_rule ctxt name rule' bad_concl);
   18.83 -    ((name, att), arule)
   18.84 +    ((binding, att), arule)
   18.85    end;
   18.86  
   18.87  val rulify =
   18.88 @@ -635,13 +640,15 @@
   18.89  
   18.90      (* add definiton of recursive predicates to theory *)
   18.91  
   18.92 -    val rec_name = if alt_name = "" then
   18.93 -      space_implode "_" (map fst cnames_syn) else alt_name;
   18.94 +    val rec_name =
   18.95 +      if Name.name_of alt_name = "" then
   18.96 +        Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
   18.97 +      else alt_name;
   18.98  
   18.99      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
  18.100        LocalTheory.define Thm.internalK
  18.101          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
  18.102 -         (("", []), fold_rev lambda params
  18.103 +         ((Name.no_binding, []), fold_rev lambda params
  18.104             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
  18.105      val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
  18.106        (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
  18.107 @@ -652,7 +659,7 @@
  18.108            val xs = map Free (Variable.variant_frees ctxt intr_ts
  18.109              (mk_names "x" (length Ts) ~~ Ts))
  18.110          in
  18.111 -          (name_mx, (("", []), fold_rev lambda (params @ xs)
  18.112 +          (name_mx, ((Name.no_binding, []), fold_rev lambda (params @ xs)
  18.113              (list_comb (rec_const, params @ make_bool_args' bs i @
  18.114                make_args argTs (xs ~~ Ts)))))
  18.115          end) (cnames_syn ~~ cs);
  18.116 @@ -665,9 +672,12 @@
  18.117      list_comb (rec_const, params), preds, argTs, bs, xs)
  18.118    end;
  18.119  
  18.120 -fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts
  18.121 +fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
  18.122        elims raw_induct ctxt =
  18.123    let
  18.124 +    val rec_name = Name.name_of rec_binding;
  18.125 +    val rec_qualified = NameSpace.qualified rec_name;
  18.126 +    val intr_names = map Name.name_of intr_bindings;
  18.127      val ind_case_names = RuleCases.case_names intr_names;
  18.128      val induct =
  18.129        if coind then
  18.130 @@ -681,28 +691,28 @@
  18.131      val (intrs', ctxt1) =
  18.132        ctxt |>
  18.133        LocalTheory.notes kind
  18.134 -        (map (NameSpace.qualified rec_name) intr_names ~~
  18.135 +        (map (Name.map_name rec_qualified) intr_bindings ~~
  18.136           intr_atts ~~ map (fn th => [([th],
  18.137             [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
  18.138        map (hd o snd);
  18.139      val (((_, elims'), (_, [induct'])), ctxt2) =
  18.140        ctxt1 |>
  18.141 -      LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
  18.142 +      LocalTheory.note kind ((Name.binding (rec_qualified "intros"), []), intrs') ||>>
  18.143        fold_map (fn (name, (elim, cases)) =>
  18.144 -        LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
  18.145 +        LocalTheory.note kind ((Name.binding (NameSpace.qualified (Sign.base_name name) "cases"),
  18.146            [Attrib.internal (K (RuleCases.case_names cases)),
  18.147             Attrib.internal (K (RuleCases.consumes 1)),
  18.148             Attrib.internal (K (Induct.cases_pred name)),
  18.149             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
  18.150          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
  18.151 -      LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
  18.152 +      LocalTheory.note kind ((Name.binding (rec_qualified (coind_prefix coind ^ "induct")),
  18.153          map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
  18.154  
  18.155      val ctxt3 = if no_ind orelse coind then ctxt2 else
  18.156        let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
  18.157        in
  18.158          ctxt2 |>
  18.159 -        LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []),
  18.160 +        LocalTheory.notes kind [((Name.binding (rec_qualified "inducts"), []),
  18.161            inducts |> map (fn (name, th) => ([th],
  18.162              [Attrib.internal (K ind_case_names),
  18.163               Attrib.internal (K (RuleCases.consumes 1)),
  18.164 @@ -711,24 +721,25 @@
  18.165    in (intrs', elims', induct', ctxt3) end;
  18.166  
  18.167  type inductive_flags =
  18.168 -  {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
  18.169 +  {quiet_mode: bool, verbose: bool, kind: string, alt_name: Name.binding,
  18.170     coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
  18.171  
  18.172  type add_ind_def =
  18.173    inductive_flags ->
  18.174 -  term list -> ((string * Attrib.src list) * term) list -> thm list ->
  18.175 -  term list -> (string * mixfix) list ->
  18.176 +  term list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
  18.177 +  term list -> (Name.binding * mixfix) list ->
  18.178    local_theory -> inductive_result * local_theory
  18.179  
  18.180 -fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
  18.181 +fun (add_ind_def: add_ind_def)
  18.182 +    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
  18.183      cs intros monos params cnames_syn ctxt =
  18.184    let
  18.185      val _ = null cnames_syn andalso error "No inductive predicates given";
  18.186 +    val names = map (Name.name_of o fst) cnames_syn;
  18.187      val _ = message (quiet_mode andalso not verbose)
  18.188 -      ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
  18.189 -        commas_quote (map fst cnames_syn));
  18.190 +      ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
  18.191  
  18.192 -    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;  (* FIXME *)
  18.193 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn;  (* FIXME *)
  18.194      val ((intr_names, intr_atts), intr_ts) =
  18.195        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
  18.196  
  18.197 @@ -739,7 +750,8 @@
  18.198      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
  18.199        params intr_ts rec_preds_defs ctxt1;
  18.200      val elims = if no_elim then [] else
  18.201 -      prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt1;
  18.202 +      prove_elims quiet_mode cs params intr_ts (map Name.name_of intr_names)
  18.203 +        unfold rec_preds_defs ctxt1;
  18.204      val raw_induct = zero_var_indexes
  18.205        (if no_ind then Drule.asm_rl else
  18.206         if coind then
  18.207 @@ -755,7 +767,6 @@
  18.208      val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
  18.209        cnames intrs intr_names intr_atts elims raw_induct ctxt1;
  18.210  
  18.211 -    val names = map #1 cnames_syn;
  18.212      val result =
  18.213        {preds = preds,
  18.214         intrs = intrs',
  18.215 @@ -782,35 +793,35 @@
  18.216  
  18.217      (* abbrevs *)
  18.218  
  18.219 -    val (_, ctxt1) = Variable.add_fixes (map (fst o fst) cnames_syn) lthy;
  18.220 +    val (_, ctxt1) = Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn) lthy;
  18.221  
  18.222      fun get_abbrev ((name, atts), t) =
  18.223        if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
  18.224          let
  18.225 -          val _ = name = "" andalso null atts orelse
  18.226 +          val _ = Name.name_of name = "" andalso null atts orelse
  18.227              error "Abbreviations may not have names or attributes";
  18.228            val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
  18.229 -          val mx =
  18.230 -            (case find_first (fn ((c, _), _) => c = x) cnames_syn of
  18.231 +          val var =
  18.232 +            (case find_first (fn ((c, _), _) => Name.name_of c = x) cnames_syn of
  18.233                NONE => error ("Undeclared head of abbreviation " ^ quote x)
  18.234 -            | SOME ((_, T'), mx) =>
  18.235 +            | SOME ((b, T'), mx) =>
  18.236                  if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
  18.237 -                else mx);
  18.238 -        in SOME ((x, mx), rhs) end
  18.239 +                else (b, mx));
  18.240 +        in SOME (var, rhs) end
  18.241        else NONE;
  18.242  
  18.243      val abbrevs = map_filter get_abbrev spec;
  18.244 -    val bs = map (fst o fst) abbrevs;
  18.245 +    val bs = map (Name.name_of o fst o fst) abbrevs;
  18.246  
  18.247  
  18.248      (* predicates *)
  18.249  
  18.250      val pre_intros = filter_out (is_some o get_abbrev) spec;
  18.251 -    val cnames_syn' = filter_out (member (op =) bs o fst o fst) cnames_syn;
  18.252 -    val cs = map (Free o fst) cnames_syn';
  18.253 +    val cnames_syn' = filter_out (member (op =) bs o Name.name_of o fst o fst) cnames_syn;
  18.254 +    val cs = map (Free o apfst Name.name_of o fst) cnames_syn';
  18.255      val ps = map Free pnames;
  18.256  
  18.257 -    val (_, ctxt2) = lthy |> Variable.add_fixes (map (fst o fst) cnames_syn');
  18.258 +    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn');
  18.259      val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
  18.260      val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
  18.261      val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
  18.262 @@ -837,12 +848,12 @@
  18.263      val (cs, ps) = chop (length cnames_syn) vars;
  18.264      val intrs = map (apsnd the_single) specs;
  18.265      val monos = Attrib.eval_thms lthy raw_monos;
  18.266 -    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK, alt_name = "",
  18.267 -      coind = coind, no_elim = false, no_ind = false, skip_mono = false};
  18.268 +    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
  18.269 +      alt_name = Name.no_binding, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
  18.270    in
  18.271      lthy
  18.272      |> LocalTheory.set_group (serial_string ())
  18.273 -    |> gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos
  18.274 +    |> gen_add_inductive_i mk_def flags cs (map (apfst Name.name_of o fst) ps) intrs monos
  18.275    end;
  18.276  
  18.277  val add_inductive_i = gen_add_inductive_i add_ind_def;
  18.278 @@ -850,7 +861,7 @@
  18.279  
  18.280  fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
  18.281    let
  18.282 -    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
  18.283 +    val name = Sign.full_name thy (Name.name_of (fst (fst (hd cnames_syn))));
  18.284      val ctxt' = thy
  18.285        |> TheoryTarget.init NONE
  18.286        |> LocalTheory.set_group group
  18.287 @@ -934,14 +945,15 @@
  18.288  
  18.289  val _ = OuterKeyword.keyword "monos";
  18.290  
  18.291 +(* FIXME eliminate *)
  18.292  fun flatten_specification specs = specs |> maps
  18.293    (fn (a, (concl, [])) => concl |> map
  18.294          (fn ((b, atts), [B]) =>
  18.295 -              if a = "" then ((b, atts), B)
  18.296 -              else if b = "" then ((a, atts), B)
  18.297 -              else error ("Illegal nested case names " ^ quote (NameSpace.append a b))
  18.298 -          | ((b, _), _) => error ("Illegal simultaneous specification " ^ quote b))
  18.299 -    | (a, _) => error ("Illegal local specification parameters for " ^ quote a));
  18.300 +              if Name.name_of a = "" then ((b, atts), B)
  18.301 +              else if Name.name_of b = "" then ((a, atts), B)
  18.302 +              else error "Illegal nested case names"
  18.303 +          | ((b, _), _) => error "Illegal simultaneous specification")
  18.304 +    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Name.name_of a)));
  18.305  
  18.306  fun gen_ind_decl mk_def coind =
  18.307    P.fixes -- P.for_fixes --
    19.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Sep 02 14:10:32 2008 +0200
    19.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Sep 02 14:10:45 2008 +0200
    19.3 @@ -337,9 +337,7 @@
    19.4              (Logic.strip_assums_concl rintr));
    19.5            val s' = Sign.base_name s;
    19.6            val T' = Logic.unvarifyT T
    19.7 -        in (((s', T'), NoSyn),
    19.8 -          (Const (s, T'), Free (s', T')))
    19.9 -        end) rintrs));
   19.10 +        in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
   19.11      val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
   19.12        (List.take (snd (strip_comb
   19.13          (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
   19.14 @@ -348,10 +346,10 @@
   19.15  
   19.16      val (ind_info, thy3') = thy2 |>
   19.17        InductivePackage.add_inductive_global (serial_string ())
   19.18 -        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = "",
   19.19 +        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
   19.20            coind = false, no_elim = false, no_ind = false, skip_mono = false}
   19.21          rlzpreds rlzparams (map (fn (rintr, intr) =>
   19.22 -          ((Sign.base_name (name_of_thm intr), []),
   19.23 +          ((Name.binding (Sign.base_name (name_of_thm intr)), []),
   19.24             subst_atomic rlzpreds' (Logic.unvarify rintr)))
   19.25               (rintrs ~~ maps snd rss)) [] ||>
   19.26        Sign.absolute_path;
    20.1 --- a/src/HOL/Tools/inductive_set_package.ML	Tue Sep 02 14:10:32 2008 +0200
    20.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Tue Sep 02 14:10:45 2008 +0200
    20.3 @@ -13,12 +13,12 @@
    20.4    val pred_set_conv_att: attribute
    20.5    val add_inductive_i:
    20.6      InductivePackage.inductive_flags ->
    20.7 -    ((string * typ) * mixfix) list ->
    20.8 -    (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    20.9 +    ((Name.binding * typ) * mixfix) list ->
   20.10 +    (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
   20.11        local_theory -> InductivePackage.inductive_result * local_theory
   20.12 -  val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
   20.13 -    (string * string option * mixfix) list ->
   20.14 -    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
   20.15 +  val add_inductive: bool -> bool -> (Name.binding * string option * mixfix) list ->
   20.16 +    (Name.binding * string option * mixfix) list ->
   20.17 +    ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
   20.18      local_theory -> InductivePackage.inductive_result * local_theory
   20.19    val setup: theory -> theory
   20.20  end;
   20.21 @@ -461,16 +461,17 @@
   20.22             | NONE => u)) |>
   20.23          Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
   20.24          eta_contract (member op = cs' orf is_pred pred_arities))) intros;
   20.25 -    val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn;
   20.26 +    val cnames_syn' = map (fn (b, _) => (Name.map_name (suffix "p") b, NoSyn)) cnames_syn;
   20.27      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
   20.28      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
   20.29 -      InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind,
   20.30 -          alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
   20.31 +      InductivePackage.add_ind_def
   20.32 +        {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Name.no_binding,
   20.33 +          coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
   20.34          cs' intros' monos' params1 cnames_syn' ctxt;
   20.35  
   20.36      (* define inductive sets using previously defined predicates *)
   20.37      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
   20.38 -      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []),
   20.39 +      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, ((Name.no_binding, []),
   20.40           fold_rev lambda params (HOLogic.Collect_const U $
   20.41             HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
   20.42           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
   20.43 @@ -488,15 +489,17 @@
   20.44              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   20.45                [def, mem_Collect_eq, split_conv]) 1))
   20.46          in
   20.47 -          ctxt |> LocalTheory.note kind ((s ^ "p_" ^ s ^ "_eq",
   20.48 +          ctxt |> LocalTheory.note kind ((Name.binding (s ^ "p_" ^ s ^ "_eq"),
   20.49              [Attrib.internal (K pred_set_conv_att)]),
   20.50                [conv_thm]) |> snd
   20.51          end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
   20.52  
   20.53      (* convert theorems to set notation *)
   20.54 -    val rec_name = if alt_name = "" then
   20.55 -      space_implode "_" (map fst cnames_syn) else alt_name;
   20.56 -    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn;  (* FIXME *)
   20.57 +    val rec_name =
   20.58 +      if Name.name_of alt_name = "" then
   20.59 +        Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
   20.60 +      else alt_name;
   20.61 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
   20.62      val (intr_names, intr_atts) = split_list (map fst intros);
   20.63      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
   20.64      val (intrs', elims', induct, ctxt4) =
    21.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Sep 02 14:10:32 2008 +0200
    21.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Sep 02 14:10:45 2008 +0200
    21.3 @@ -8,13 +8,13 @@
    21.4  
    21.5  signature PRIMREC_PACKAGE =
    21.6  sig
    21.7 -  val add_primrec: (string * typ option * mixfix) list ->
    21.8 -    ((bstring * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
    21.9 -  val add_primrec_global: (string * typ option * mixfix) list ->
   21.10 -    ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
   21.11 +  val add_primrec: (Name.binding * typ option * mixfix) list ->
   21.12 +    ((Name.binding * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
   21.13 +  val add_primrec_global: (Name.binding * typ option * mixfix) list ->
   21.14 +    ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
   21.15    val add_primrec_overloaded: (string * (string * typ) * bool) list ->
   21.16 -    (string * typ option * mixfix) list ->
   21.17 -    ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
   21.18 +    (Name.binding * typ option * mixfix) list ->
   21.19 +    ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
   21.20  end;
   21.21  
   21.22  structure PrimrecPackage : PRIMREC_PACKAGE =
   21.23 @@ -189,14 +189,14 @@
   21.24  fun make_def ctxt fixes fs (fname, ls, rec_name, tname) =
   21.25    let
   21.26      val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t))
   21.27 -                    ((map snd ls) @ [dummyT])
   21.28 +                    (map snd ls @ [dummyT])
   21.29                      (list_comb (Const (rec_name, dummyT),
   21.30 -                                fs @ map Bound (0 ::(length ls downto 1))))
   21.31 +                                fs @ map Bound (0 :: (length ls downto 1))))
   21.32      val def_name = Thm.def_name (Sign.base_name fname);
   21.33      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
   21.34 -    val SOME mfx = get_first
   21.35 -      (fn ((v, _), mfx) => if v = fname then SOME mfx else NONE) fixes;
   21.36 -  in ((fname, mfx), ((def_name, []), rhs)) end;
   21.37 +    val SOME var = get_first (fn ((b, _), mx) =>
   21.38 +      if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
   21.39 +  in (var, ((Name.binding def_name, []), rhs)) end;
   21.40  
   21.41  
   21.42  (* find datatypes which contain all datatypes in tnames' *)
   21.43 @@ -226,16 +226,15 @@
   21.44      val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
   21.45      fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
   21.46      val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
   21.47 -  in map (fn (name_attr, t) => (name_attr, [Goal.prove ctxt [] [] t tac])) end;
   21.48 +  in map (fn (a, t) => (a, [Goal.prove ctxt [] [] t tac])) end;
   21.49  
   21.50  fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
   21.51    let
   21.52      val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
   21.53      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
   21.54 -      orelse exists (fn ((w, _), _) => v = w) fixes) o snd) spec [];
   21.55 +      orelse exists (fn ((w, _), _) => v = Name.name_of w) fixes) o snd) spec [];
   21.56      val tnames = distinct (op =) (map (#1 o snd) eqns);
   21.57 -    val dts = find_dts (DatatypePackage.get_datatypes
   21.58 -      (ProofContext.theory_of lthy)) tnames tnames;
   21.59 +    val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
   21.60      val main_fns = map (fn (tname, {index, ...}) =>
   21.61        (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
   21.62      val {descr, rec_names, rec_rewrites, ...} =
   21.63 @@ -251,7 +250,7 @@
   21.64          "\nare not mutually recursive");
   21.65      val qualify = NameSpace.qualified
   21.66        (space_implode "_" (map (Sign.base_name o #1) defs));
   21.67 -    val spec' = (map o apfst o apfst) qualify spec;
   21.68 +    val spec' = (map o apfst o apfst o Name.map_name) qualify spec;
   21.69      val simp_atts = map (Attrib.internal o K)
   21.70        [Simplifier.simp_add, RecfunCodegen.add NONE];
   21.71    in
   21.72 @@ -261,7 +260,7 @@
   21.73      |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
   21.74      |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
   21.75      |-> (fn simps' => LocalTheory.note Thm.theoremK
   21.76 -          ((qualify "simps", simp_atts), maps snd simps'))
   21.77 +          ((Name.binding (qualify "simps"), simp_atts), maps snd simps'))
   21.78      |>> snd
   21.79    end handle PrimrecError (msg, some_eqn) =>
   21.80      error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
   21.81 @@ -300,7 +299,7 @@
   21.82        P.name >> pair false) --| P.$$$ ")")) (false, "");
   21.83  
   21.84  val old_primrec_decl =
   21.85 -  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
   21.86 +  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop);
   21.87  
   21.88  fun pipe_error t = P.!!! (Scan.fail_with (K
   21.89    (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
    22.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Sep 02 14:10:32 2008 +0200
    22.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 02 14:10:45 2008 +0200
    22.3 @@ -268,8 +268,8 @@
    22.4        error ("No termination condition #" ^ string_of_int i ^
    22.5          " in recdef definition of " ^ quote name);
    22.6    in
    22.7 -    Specification.theorem Thm.internalK NONE (K I) (bname, atts)
    22.8 -      [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    22.9 +    Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
   22.10 +      [] (Element.Shows [((Name.no_binding, []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   22.11    end;
   22.12  
   22.13  val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
   22.14 @@ -299,7 +299,8 @@
   22.15  
   22.16  val recdef_decl =
   22.17    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
   22.18 -  P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
   22.19 +  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
   22.20 +    -- Scan.option hints
   22.21    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
   22.22  
   22.23  val _ =
   22.24 @@ -319,7 +320,8 @@
   22.25  val _ =
   22.26    OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
   22.27      K.thy_goal
   22.28 -    (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
   22.29 +    ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
   22.30 +        Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
   22.31        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
   22.32  
   22.33  end;
    23.1 --- a/src/HOL/Tools/specification_package.ML	Tue Sep 02 14:10:32 2008 +0200
    23.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Sep 02 14:10:45 2008 +0200
    23.3 @@ -233,7 +233,7 @@
    23.4  
    23.5  val specification_decl =
    23.6    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    23.7 -          Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
    23.8 +          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
    23.9  
   23.10  val _ =
   23.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   23.12 @@ -244,7 +244,7 @@
   23.13  val ax_specification_decl =
   23.14      P.name --
   23.15      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   23.16 -           Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
   23.17 +           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
   23.18  
   23.19  val _ =
   23.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
    24.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 02 14:10:32 2008 +0200
    24.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 02 14:10:45 2008 +0200
    24.3 @@ -134,7 +134,7 @@
    24.4            (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
    24.5          val def' = Syntax.check_term lthy def;
    24.6          val ((_, (_, thm)), lthy') = Specification.definition
    24.7 -          (NONE, (("", []), def')) lthy;
    24.8 +          (NONE, ((Name.no_binding, []), def')) lthy;
    24.9          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   24.10          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   24.11        in (thm', lthy') end;
    25.1 --- a/src/HOL/Typedef.thy	Tue Sep 02 14:10:32 2008 +0200
    25.2 +++ b/src/HOL/Typedef.thy	Tue Sep 02 14:10:45 2008 +0200
    25.3 @@ -145,7 +145,7 @@
    25.4      thy
    25.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
    25.6      |> `(fn lthy => Syntax.check_term lthy eq)
    25.7 -    |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
    25.8 +    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
    25.9      |> snd
   25.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   25.11      |> LocalTheory.exit
    26.1 --- a/src/HOL/ex/Quickcheck.thy	Tue Sep 02 14:10:32 2008 +0200
    26.2 +++ b/src/HOL/ex/Quickcheck.thy	Tue Sep 02 14:10:45 2008 +0200
    26.3 @@ -128,11 +128,11 @@
    26.4            thy
    26.5            |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
    26.6            |> PrimrecPackage.add_primrec
    26.7 -               [(fst (dest_Free random'), SOME (snd (dest_Free random')), NoSyn)]
    26.8 -                 (map (fn eq => (("", [del_func]), eq)) eqs')
    26.9 +               [(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
   26.10 +                 (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
   26.11            |-> add_code
   26.12            |> `(fn lthy => Syntax.check_term lthy eq)
   26.13 -          |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
   26.14 +          |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
   26.15            |> snd
   26.16            |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   26.17            |> LocalTheory.exit
   26.18 @@ -261,7 +261,7 @@
   26.19    in
   26.20      thy
   26.21      |> TheoryTarget.init NONE
   26.22 -    |> Specification.definition (NONE, (("", []), eq))
   26.23 +    |> Specification.definition (NONE, ((Name.no_binding, []), eq))
   26.24      |> snd
   26.25      |> LocalTheory.exit
   26.26      |> ProofContext.theory_of
    27.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 02 14:10:32 2008 +0200
    27.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 02 14:10:45 2008 +0200
    27.3 @@ -9,10 +9,10 @@
    27.4  sig
    27.5    val legacy_infer_term: theory -> term -> term
    27.6    val legacy_infer_prop: theory -> term -> term
    27.7 -  val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
    27.8 -  val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
    27.9 -  val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
   27.10 -  val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
   27.11 +  val add_fixrec: bool -> ((Name.binding * Attrib.src list) * string) list list -> theory -> theory
   27.12 +  val add_fixrec_i: bool -> ((Name.binding * attribute list) * term) list list -> theory -> theory
   27.13 +  val add_fixpat: (Name.binding * Attrib.src list) * string list -> theory -> theory
   27.14 +  val add_fixpat_i: (Name.binding * attribute list) * term list -> theory -> theory
   27.15  end;
   27.16  
   27.17  structure FixrecPackage: FIXREC_PACKAGE =
   27.18 @@ -226,7 +226,8 @@
   27.19      val eqns = List.concat blocks;
   27.20      val lengths = map length blocks;
   27.21      
   27.22 -    val ((names, srcss), strings) = apfst split_list (split_list eqns);
   27.23 +    val ((bindings, srcss), strings) = apfst split_list (split_list eqns);
   27.24 +    val names = map Name.name_of bindings;
   27.25      val atts = map (map (prep_attrib thy)) srcss;
   27.26      val eqn_ts = map (prep_prop thy) strings;
   27.27      val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
   27.28 @@ -278,7 +279,7 @@
   27.29      val ts = map (prep_term thy) strings;
   27.30      val simps = map (fix_pat thy) ts;
   27.31    in
   27.32 -    (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   27.33 +    (snd o PureThy.add_thmss [((Name.name_of name, simps), atts)]) thy
   27.34    end;
   27.35  
   27.36  val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
    28.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Tue Sep 02 14:10:32 2008 +0200
    28.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Sep 02 14:10:45 2008 +0200
    28.3 @@ -94,7 +94,7 @@
    28.4            |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
    28.5          val less_def' = Syntax.check_term lthy3 less_def;
    28.6          val ((_, (_, less_definition')), lthy4) = lthy3
    28.7 -          |> Specification.definition (NONE, (("less_" ^ name ^ "_def", []), less_def'));
    28.8 +          |> Specification.definition (NONE, ((Name.binding ("less_" ^ name ^ "_def"), []), less_def'));
    28.9          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
   28.10          val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
   28.11          val thy5 = lthy4
    29.1 --- a/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:32 2008 +0200
    29.2 +++ b/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:45 2008 +0200
    29.3 @@ -110,7 +110,8 @@
    29.4  fun attribute thy = attribute_i thy o intern_src thy;
    29.5  
    29.6  fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
    29.7 -    [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
    29.8 +    [((Name.no_binding, []),
    29.9 +      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
   29.10    |> fst |> maps snd;
   29.11  
   29.12  
    30.1 --- a/src/Pure/Isar/class.ML	Tue Sep 02 14:10:32 2008 +0200
    30.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 02 14:10:45 2008 +0200
    30.3 @@ -19,7 +19,7 @@
    30.4    val abbrev: class -> Syntax.mode -> Properties.T
    30.5      -> (string * mixfix) * term -> theory -> theory
    30.6    val note: class -> string
    30.7 -    -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    30.8 +    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
    30.9      -> theory -> (bstring * thm list) list * theory
   30.10    val declaration: class -> declaration -> theory -> theory
   30.11    val refresh_syntax: class -> Proof.context -> Proof.context
   30.12 @@ -48,7 +48,7 @@
   30.13  
   30.14    (*old axclass layer*)
   30.15    val axclass_cmd: bstring * xstring list
   30.16 -    -> ((bstring * Attrib.src list) * string list) list
   30.17 +    -> ((Name.binding * Attrib.src list) * string list) list
   30.18      -> theory -> class * theory
   30.19    val classrel_cmd: xstring * xstring -> theory -> Proof.state
   30.20  
   30.21 @@ -374,7 +374,7 @@
   30.22      thy
   30.23      |> fold2 add_constraint (map snd consts) no_constraints
   30.24      |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
   30.25 -          (inst, map (fn def => (("", []), def)) defs)
   30.26 +          (inst, map (fn def => ((Name.no_binding, []), def)) defs)
   30.27      |> fold2 add_constraint (map snd consts) constraints
   30.28    end;
   30.29  
   30.30 @@ -569,7 +569,7 @@
   30.31      val constrain = Element.Constrains ((map o apsnd o map_atyps)
   30.32        (K (TFree (Name.aT, base_sort))) supparams);
   30.33      fun fork_syn (Element.Fixes xs) =
   30.34 -          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   30.35 +          fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs
   30.36            #>> Element.Fixes
   30.37        | fork_syn x = pair x;
   30.38      fun fork_syntax elems =
   30.39 @@ -628,7 +628,7 @@
   30.40      |> add_consts ((snd o chop (length supparams)) all_params)
   30.41      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   30.42            (map (fst o snd) params)
   30.43 -          [((bname ^ "_" ^ AxClass.axiomsN, []), map (globalize param_map) raw_pred)]
   30.44 +          [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
   30.45      #> snd
   30.46      #> `get_axiom
   30.47      #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
    31.1 --- a/src/Pure/Isar/constdefs.ML	Tue Sep 02 14:10:32 2008 +0200
    31.2 +++ b/src/Pure/Isar/constdefs.ML	Tue Sep 02 14:10:45 2008 +0200
    31.3 @@ -9,12 +9,12 @@
    31.4  
    31.5  signature CONSTDEFS =
    31.6  sig
    31.7 -  val add_constdefs: (string * string option) list *
    31.8 -    ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
    31.9 -    theory -> theory
   31.10 -  val add_constdefs_i: (string * typ option) list *
   31.11 -    ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
   31.12 -    theory -> theory
   31.13 +  val add_constdefs: (Name.binding * string option) list *
   31.14 +    ((Name.binding * string option * mixfix) option *
   31.15 +      ((Name.binding * Attrib.src list) * string)) list -> theory -> theory
   31.16 +  val add_constdefs_i: (Name.binding * typ option) list *
   31.17 +    ((Name.binding * typ option * mixfix) option *
   31.18 +      ((Name.binding * attribute list) * term)) list -> theory -> theory
   31.19  end;
   31.20  
   31.21  structure Constdefs: CONSTDEFS =
   31.22 @@ -38,13 +38,16 @@
   31.23  
   31.24      val prop = prep_prop var_ctxt raw_prop;
   31.25      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
   31.26 -    val _ = (case d of NONE => () | SOME c' =>
   31.27 -      if c <> c' then
   31.28 -        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
   31.29 -      else ());
   31.30 +    val _ =
   31.31 +      (case Option.map Name.name_of d of
   31.32 +        NONE => ()
   31.33 +      | SOME c' =>
   31.34 +          if c <> c' then
   31.35 +            err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
   31.36 +          else ());
   31.37  
   31.38      val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
   31.39 -    val name = Thm.def_name_optional c raw_name;
   31.40 +    val name = Thm.def_name_optional c (Name.name_of raw_name);
   31.41      val atts = map (prep_att thy) raw_atts;
   31.42  
   31.43      val thy' =
    32.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 02 14:10:32 2008 +0200
    32.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 02 14:10:45 2008 +0200
    32.3 @@ -15,19 +15,19 @@
    32.4    val print_ast_translation: bool * (string * Position.T) -> theory -> theory
    32.5    val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
    32.6      theory -> theory
    32.7 -  val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    32.8 -  val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    32.9 +  val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
   32.10 +  val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
   32.11    val declaration: string * Position.T -> local_theory -> local_theory
   32.12    val simproc_setup: string -> string list -> string * Position.T -> string list ->
   32.13      local_theory -> local_theory
   32.14    val hide_names: bool -> string * xstring list -> theory -> theory
   32.15 -  val have: ((string * Attrib.src list) * (string * string list) list) list ->
   32.16 +  val have: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   32.17      bool -> Proof.state -> Proof.state
   32.18 -  val hence: ((string * Attrib.src list) * (string * string list) list) list ->
   32.19 +  val hence: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   32.20      bool -> Proof.state -> Proof.state
   32.21 -  val show: ((string * Attrib.src list) * (string * string list) list) list ->
   32.22 +  val show: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   32.23      bool -> Proof.state -> Proof.state
   32.24 -  val thus: ((string * Attrib.src list) * (string * string list) list) list ->
   32.25 +  val thus: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   32.26      bool -> Proof.state -> Proof.state
   32.27    val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
   32.28    val terminal_proof: Method.text * Method.text option ->
   32.29 @@ -179,7 +179,7 @@
   32.30  (* axioms *)
   32.31  
   32.32  fun add_axms f args thy =
   32.33 -  f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
   32.34 +  f (map (fn ((b, ax), srcs) => ((Name.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
   32.35  
   32.36  val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
   32.37  
    33.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 02 14:10:32 2008 +0200
    33.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 02 14:10:45 2008 +0200
    33.3 @@ -203,10 +203,10 @@
    33.4  (* old constdefs *)
    33.5  
    33.6  val old_constdecl =
    33.7 -  P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
    33.8 -  P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
    33.9 +  P.binding --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
   33.10 +  P.binding -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
   33.11      --| Scan.option P.where_ >> P.triple1 ||
   33.12 -  P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
   33.13 +  P.binding -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
   33.14  
   33.15  val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   33.16  
   33.17 @@ -221,7 +221,7 @@
   33.18  (* constant definitions and abbreviations *)
   33.19  
   33.20  val constdecl =
   33.21 -  P.name --
   33.22 +  P.binding --
   33.23      (P.where_ >> K (NONE, NoSyn) ||
   33.24        P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
   33.25        Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
   33.26 @@ -272,7 +272,7 @@
   33.27  val _ =
   33.28    OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
   33.29      (P.and_list1 SpecParse.xthms1
   33.30 -      >> (fn args => #2 o Specification.theorems_cmd "" [(("", []), flat args)]));
   33.31 +      >> (fn args => #2 o Specification.theorems_cmd "" [((Name.no_binding, []), flat args)]));
   33.32  
   33.33  
   33.34  (* name space entry path *)
   33.35 @@ -396,16 +396,18 @@
   33.36      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
   33.37        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
   33.38        SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   33.39 -        >> (fn ((x, y), z) => Toplevel.print o
   33.40 -            Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
   33.41 +        >> (fn (((name, atts), expr), insts) => Toplevel.print o
   33.42 +            Toplevel.theory_to_proof
   33.43 +              (Locale.interpretation I ((true, Name.name_of name), atts) expr insts)));
   33.44  
   33.45  val _ =
   33.46    OuterSyntax.command "interpret"
   33.47      "prove and register interpretation of locale expression in proof context"
   33.48      (K.tag_proof K.prf_goal)
   33.49      (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   33.50 -      >> (fn ((x, y), z) => Toplevel.print o
   33.51 -          Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
   33.52 +      >> (fn (((name, atts), expr), insts) => Toplevel.print o
   33.53 +          Toplevel.proof'
   33.54 +            (Locale.interpret Seq.single ((true, Name.name_of name), atts) expr insts)));
   33.55  
   33.56  
   33.57  (* classes *)
   33.58 @@ -466,7 +468,7 @@
   33.59  fun gen_theorem kind =
   33.60    OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
   33.61      (Scan.optional (SpecParse.opt_thm_name ":" --|
   33.62 -      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
   33.63 +      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) (Name.no_binding, []) --
   33.64        SpecParse.general_statement >> (fn (a, (elems, concl)) =>
   33.65          (Specification.theorem_cmd kind NONE (K I) a elems concl)));
   33.66  
   33.67 @@ -552,7 +554,7 @@
   33.68      (K.tag_proof K.prf_asm)
   33.69      (P.and_list1
   33.70        (SpecParse.opt_thm_name ":" --
   33.71 -        ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   33.72 +        ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   33.73      >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
   33.74  
   33.75  val _ =
    34.1 --- a/src/Pure/Isar/local_defs.ML	Tue Sep 02 14:10:32 2008 +0200
    34.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Sep 02 14:10:45 2008 +0200
    34.3 @@ -12,10 +12,11 @@
    34.4    val mk_def: Proof.context -> (string * term) list -> term list
    34.5    val expand: cterm list -> thm -> thm
    34.6    val def_export: Assumption.export
    34.7 -  val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
    34.8 -    (term * (bstring * thm)) list * Proof.context
    34.9 -  val add_def: (string * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   34.10 -  val fixed_abbrev: (string * mixfix) * term -> Proof.context -> (term * term) * Proof.context
   34.11 +  val add_defs: ((Name.binding * mixfix) * ((Name.binding * attribute list) * term)) list ->
   34.12 +    Proof.context -> (term * (string * thm)) list * Proof.context
   34.13 +  val add_def: (Name.binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   34.14 +  val fixed_abbrev: (Name.binding * mixfix) * term -> Proof.context ->
   34.15 +    (term * term) * Proof.context
   34.16    val export: Proof.context -> Proof.context -> thm -> thm list * thm
   34.17    val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
   34.18    val trans_terms: Proof.context -> thm list -> thm
   34.19 @@ -88,22 +89,23 @@
   34.20  
   34.21  fun add_defs defs ctxt =
   34.22    let
   34.23 -    val ((xs, mxs), specs) = defs |> split_list |>> split_list;
   34.24 -    val ((names, atts), rhss) = specs |> split_list |>> split_list;
   34.25 -    val names' = map2 Thm.def_name_optional xs names;
   34.26 +    val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
   34.27 +    val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
   34.28 +    val xs = map Name.name_of bvars;
   34.29 +    val names = map2 (Name.map_name o Thm.def_name_optional) xs bfacts;
   34.30      val eqs = mk_def ctxt (xs ~~ rhss);
   34.31      val lhss = map (fst o Logic.dest_equals) eqs;
   34.32    in
   34.33      ctxt
   34.34 -    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
   34.35 +    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
   34.36      |> fold Variable.declare_term eqs
   34.37      |> ProofContext.add_assms_i def_export
   34.38 -      (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs)
   34.39 +      (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
   34.40      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   34.41    end;
   34.42  
   34.43  fun add_def (var, rhs) ctxt =
   34.44 -  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (("", []), rhs))] ctxt
   34.45 +  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Name.no_binding, []), rhs))] ctxt
   34.46    in ((lhs, th), ctxt') end;
   34.47  
   34.48  
    35.1 --- a/src/Pure/Isar/local_theory.ML	Tue Sep 02 14:10:32 2008 +0200
    35.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Sep 02 14:10:45 2008 +0200
    35.3 @@ -26,16 +26,16 @@
    35.4    val affirm: local_theory -> local_theory
    35.5    val pretty: local_theory -> Pretty.T list
    35.6    val axioms: string ->
    35.7 -    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    35.8 -    -> (term list * (bstring * thm list) list) * local_theory
    35.9 -  val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
   35.10 +    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
   35.11 +    -> (term list * (string * thm list) list) * local_theory
   35.12 +  val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
   35.13      (term * term) * local_theory
   35.14 -  val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
   35.15 -    (term * (bstring * thm)) * local_theory
   35.16 -  val note: string -> (bstring * Attrib.src list) * thm list ->
   35.17 -    local_theory -> (bstring * thm list) * local_theory
   35.18 -  val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   35.19 -    local_theory -> (bstring * thm list) list * local_theory
   35.20 +  val define: string -> (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
   35.21 +    (term * (string * thm)) * local_theory
   35.22 +  val note: string -> (Name.binding * Attrib.src list) * thm list ->
   35.23 +    local_theory -> (string * thm list) * local_theory
   35.24 +  val notes: string -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   35.25 +    local_theory -> (string * thm list) list * local_theory
   35.26    val type_syntax: declaration -> local_theory -> local_theory
   35.27    val term_syntax: declaration -> local_theory -> local_theory
   35.28    val declaration: declaration -> local_theory -> local_theory
   35.29 @@ -57,15 +57,15 @@
   35.30  type operations =
   35.31   {pretty: local_theory -> Pretty.T list,
   35.32    axioms: string ->
   35.33 -    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
   35.34 -    -> (term list * (bstring * thm list) list) * local_theory,
   35.35 -  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
   35.36 +    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
   35.37 +    -> (term list * (string * thm list) list) * local_theory,
   35.38 +  abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> (term * term) * local_theory,
   35.39    define: string ->
   35.40 -    (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
   35.41 -    (term * (bstring * thm)) * local_theory,
   35.42 +    (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
   35.43 +    (term * (string * thm)) * local_theory,
   35.44    notes: string ->
   35.45 -    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   35.46 -    local_theory -> (bstring * thm list) list * local_theory,
   35.47 +    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   35.48 +    local_theory -> (string * thm list) list * local_theory,
   35.49    type_syntax: declaration -> local_theory -> local_theory,
   35.50    term_syntax: declaration -> local_theory -> local_theory,
   35.51    declaration: declaration -> local_theory -> local_theory,
    36.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 02 14:10:32 2008 +0200
    36.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 02 14:10:45 2008 +0200
    36.3 @@ -55,16 +55,16 @@
    36.4    val parameters_of_expr: theory -> expr ->
    36.5      ((string * typ) * mixfix) list
    36.6    val local_asms_of: theory -> string ->
    36.7 -    ((string * Attrib.src list) * term list) list
    36.8 +    ((Name.binding * Attrib.src list) * term list) list
    36.9    val global_asms_of: theory -> string ->
   36.10 -    ((string * Attrib.src list) * term list) list
   36.11 +    ((Name.binding * Attrib.src list) * term list) list
   36.12  
   36.13    (* Theorems *)
   36.14    val intros: theory -> string -> thm list * thm list
   36.15    val dests: theory -> string -> thm list
   36.16    (* Not part of the official interface.  DO NOT USE *)
   36.17    val facts_of: theory -> string
   36.18 -    -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list list
   36.19 +    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list list
   36.20  
   36.21    (* Processing of locale statements *)
   36.22    val read_context_statement: xstring option -> Element.context element list ->
   36.23 @@ -96,7 +96,7 @@
   36.24  
   36.25    (* Storing results *)
   36.26    val add_thmss: string -> string ->
   36.27 -    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   36.28 +    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   36.29      Proof.context -> Proof.context
   36.30    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   36.31    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   36.32 @@ -104,21 +104,21 @@
   36.33  
   36.34    val interpretation_i: (Proof.context -> Proof.context) ->
   36.35      (bool * string) * Attrib.src list -> expr ->
   36.36 -    term option list * ((bstring * Attrib.src list) * term) list ->
   36.37 +    term option list * ((Name.binding * Attrib.src list) * term) list ->
   36.38      theory -> Proof.state
   36.39    val interpretation: (Proof.context -> Proof.context) ->
   36.40      (bool * string) * Attrib.src list -> expr ->
   36.41 -    string option list * ((bstring * Attrib.src list) * string) list ->
   36.42 +    string option list * ((Name.binding * Attrib.src list) * string) list ->
   36.43      theory -> Proof.state
   36.44    val interpretation_in_locale: (Proof.context -> Proof.context) ->
   36.45      xstring * expr -> theory -> Proof.state
   36.46    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
   36.47      (bool * string) * Attrib.src list -> expr ->
   36.48 -    term option list * ((bstring * Attrib.src list) * term) list ->
   36.49 +    term option list * ((Name.binding * Attrib.src list) * term) list ->
   36.50      bool -> Proof.state -> Proof.state
   36.51    val interpret: (Proof.state -> Proof.state Seq.seq) ->
   36.52      (bool * string) * Attrib.src list -> expr ->
   36.53 -    string option list * ((bstring * Attrib.src list) * string) list ->
   36.54 +    string option list * ((Name.binding * Attrib.src list) * string) list ->
   36.55      bool -> Proof.state -> Proof.state
   36.56  end;
   36.57  
   36.58 @@ -756,7 +756,7 @@
   36.59              val ren = renaming xs parms';
   36.60              (* renaming may reduce number of parameters *)
   36.61              val new_parms = map (Element.rename ren) parms' |> distinct (op =);
   36.62 -            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
   36.63 +            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
   36.64              val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
   36.65                  handle Symtab.DUP x =>
   36.66                    err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
   36.67 @@ -789,7 +789,7 @@
   36.68  fun make_raw_params_elemss (params, tenv, syn) =
   36.69      [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   36.70        Int [Fixes (map (fn p =>
   36.71 -        (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   36.72 +        (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   36.73  
   36.74  
   36.75  (* flatten_expr:
   36.76 @@ -929,7 +929,7 @@
   36.77          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   36.78          val elem_morphism =
   36.79            Element.rename_morphism ren $>
   36.80 -          Morphism.name_morphism (params_qualified params) $>
   36.81 +          Morphism.name_morphism (Name.map_name (params_qualified params)) $>
   36.82            Element.instT_morphism thy env;
   36.83          val elems' = map (Element.morph_ctxt elem_morphism) elems;
   36.84        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   36.85 @@ -978,7 +978,7 @@
   36.86          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   36.87          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
   36.88              let val ((c, _), t') = LocalDefs.cert_def ctxt t
   36.89 -            in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
   36.90 +            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
   36.91          val (_, ctxt') =
   36.92            ctxt |> fold (Variable.auto_fixes o #1) asms
   36.93            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
   36.94 @@ -989,7 +989,7 @@
   36.95        let
   36.96          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
   36.97          val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
   36.98 -      in (if is_ext then res else [], (ctxt', mode)) end;
   36.99 +      in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
  36.100  
  36.101  fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  36.102    let
  36.103 @@ -1076,15 +1076,15 @@
  36.104  *)
  36.105  
  36.106  fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
  36.107 -        val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
  36.108 +        val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
  36.109        in
  36.110          ((ids',
  36.111           merge_syntax ctxt ids'
  36.112 -           (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
  36.113 +           (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
  36.114             handle Symtab.DUP x => err_in_locale ctxt
  36.115               ("Conflicting syntax for parameter: " ^ quote x)
  36.116               (map #1 ids')),
  36.117 -         [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
  36.118 +         [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
  36.119        end
  36.120    | flatten _ ((ids, syn), Elem elem) =
  36.121        ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  36.122 @@ -1104,7 +1104,7 @@
  36.123        let val (vars, _) = prep_vars fixes ctxt
  36.124        in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
  36.125    | declare_ext_elem prep_vars (Constrains csts) ctxt =
  36.126 -      let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
  36.127 +      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
  36.128        in ([], ctxt') end
  36.129    | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
  36.130    | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
  36.131 @@ -1227,8 +1227,9 @@
  36.132        end;
  36.133  
  36.134  
  36.135 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
  36.136 -      (x, AList.lookup (op =) parms x, mx)) fixes)
  36.137 +fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
  36.138 +      let val x = Name.name_of binding
  36.139 +      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
  36.140    | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  36.141    | finish_ext_elem _ close (Assumes asms, propp) =
  36.142        close (Assumes (map #1 asms ~~ propp))
  36.143 @@ -1274,7 +1275,7 @@
  36.144      list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
  36.145        Term.fast_term_ord (d1, d2)) (defs1, defs2);
  36.146  structure Defstab =
  36.147 -    TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
  36.148 +    TableFun(type key = ((Name.binding * Attrib.src list) * (term * term list)) list
  36.149          val ord = defs_ord);
  36.150  
  36.151  fun rem_dup_defs es ds =
  36.152 @@ -1387,7 +1388,7 @@
  36.153        |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
  36.154    | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  36.155       {var = I, typ = I, term = I,
  36.156 -      name = prep_name,
  36.157 +      name = Name.map_name prep_name,
  36.158        fact = get ctxt,
  36.159        attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  36.160  
  36.161 @@ -1572,8 +1573,8 @@
  36.162  (* naming of interpreted theorems *)
  36.163  
  36.164  fun add_param_prefixss s =
  36.165 -  (map o apfst o apfst) (NameSpace.qualified s);
  36.166 -fun drop_param_prefixss args = (map o apfst o apfst)
  36.167 +  (map o apfst o apfst o Name.map_name) (NameSpace.qualified s);
  36.168 +fun drop_param_prefixss args = (map o apfst o apfst o Name.map_name)
  36.169    (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
  36.170  
  36.171  fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
  36.172 @@ -1660,7 +1661,7 @@
  36.173  
  36.174  fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
  36.175    let
  36.176 -    val inst = Morphism.name_morphism (NameSpace.qualified prfx) $>
  36.177 +    val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
  36.178  (* need to add parameter prefix *) (* FIXME *)
  36.179        Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
  36.180        Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
  36.181 @@ -1724,7 +1725,7 @@
  36.182      (fn (axiom, elems, params, decls, regs, intros, dests) =>
  36.183        (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
  36.184    add_thmss loc Thm.internalK
  36.185 -    [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  36.186 +    [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  36.187  
  36.188  in
  36.189  
  36.190 @@ -1864,12 +1865,13 @@
  36.191              thy
  36.192              |> def_pred aname parms defs exts exts';
  36.193            val elemss' = change_assumes_elemss axioms elemss;
  36.194 -          val a_elem = [(("", []), [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  36.195 +          val a_elem = [(("", []),
  36.196 +            [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  36.197            val (_, thy'') =
  36.198              thy'
  36.199              |> Sign.add_path aname
  36.200              |> Sign.no_base_names
  36.201 -            |> PureThy.note_thmss Thm.internalK [((introN, []), [([intro], [])])]
  36.202 +            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
  36.203              ||> Sign.restore_naming thy';
  36.204          in ((elemss', [statement]), a_elem, [intro], thy'') end;
  36.205      val (predicate, stmt', elemss'', b_intro, thy'''') =
  36.206 @@ -1882,14 +1884,15 @@
  36.207            val cstatement = Thm.cterm_of thy''' statement;
  36.208            val elemss'' = change_elemss_hyps axioms elemss';
  36.209            val b_elem = [(("", []),
  36.210 -               [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  36.211 +               [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  36.212            val (_, thy'''') =
  36.213              thy'''
  36.214              |> Sign.add_path pname
  36.215              |> Sign.no_base_names
  36.216              |> PureThy.note_thmss Thm.internalK
  36.217 -                 [((introN, []), [([intro], [])]),
  36.218 -                  ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  36.219 +                 [((Name.binding introN, []), [([intro], [])]),
  36.220 +                  ((Name.binding axiomsN, []),
  36.221 +                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  36.222              ||> Sign.restore_naming thy''';
  36.223          in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
  36.224    in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
  36.225 @@ -1905,7 +1908,7 @@
  36.226  
  36.227  fun defines_to_notes is_ext thy (Defines defs) defns =
  36.228      let
  36.229 -      val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
  36.230 +      val defs' = map (fn (_, (def, _)) => ((Name.no_binding, []), (def, []))) defs
  36.231        val notes = map (fn (a, (def, _)) =>
  36.232          (a, [([assume (cterm_of thy def)], [])])) defs
  36.233      in
  36.234 @@ -1994,9 +1997,9 @@
  36.235  end;
  36.236  
  36.237  val _ = Context.>> (Context.map_theory
  36.238 - (add_locale_i "" "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
  36.239 + (add_locale_i "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
  36.240    snd #> ProofContext.theory_of #>
  36.241 -  add_locale_i "" "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
  36.242 +  add_locale_i "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
  36.243    snd #> ProofContext.theory_of));
  36.244  
  36.245  
  36.246 @@ -2374,7 +2377,7 @@
  36.247              fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
  36.248                  let
  36.249                    val att_morphism =
  36.250 -                    Morphism.name_morphism (NameSpace.qualified prfx) $>
  36.251 +                    Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
  36.252                      Morphism.thm_morphism satisfy $>
  36.253                      Element.inst_morphism thy insts $>
  36.254                      Morphism.thm_morphism disch;
  36.255 @@ -2435,7 +2438,7 @@
  36.256    in
  36.257      state
  36.258      |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  36.259 -      "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
  36.260 +      "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
  36.261      |> Element.refine_witness |> Seq.hd
  36.262    end;
  36.263  
    37.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 02 14:10:32 2008 +0200
    37.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 02 14:10:45 2008 +0200
    37.3 @@ -44,26 +44,30 @@
    37.4    val match_bind_i: (term list * term) list -> state -> state
    37.5    val let_bind: (string list * string) list -> state -> state
    37.6    val let_bind_i: (term list * term) list -> state -> state
    37.7 -  val fix: (string * string option * mixfix) list -> state -> state
    37.8 -  val fix_i: (string * typ option * mixfix) list -> state -> state
    37.9 +  val fix: (Name.binding * string option * mixfix) list -> state -> state
   37.10 +  val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
   37.11    val assm: Assumption.export ->
   37.12 -    ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   37.13 +    ((Name.binding * Attrib.src list) * (string * string list) list) list -> state -> state
   37.14    val assm_i: Assumption.export ->
   37.15 -    ((string * attribute list) * (term * term list) list) list -> state -> state
   37.16 -  val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   37.17 -  val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
   37.18 -  val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   37.19 -  val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
   37.20 -  val def: ((string * Attrib.src list) *
   37.21 -    ((string * mixfix) * (string * string list))) list -> state -> state
   37.22 -  val def_i: ((string * attribute list) *
   37.23 -    ((string * mixfix) * (term * term list))) list -> state -> state
   37.24 +    ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
   37.25 +  val assume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   37.26 +    state -> state
   37.27 +  val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
   37.28 +    state -> state
   37.29 +  val presume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   37.30 +    state -> state
   37.31 +  val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
   37.32 +    state -> state
   37.33 +  val def: ((Name.binding * Attrib.src list) *
   37.34 +    ((Name.binding * mixfix) * (string * string list))) list -> state -> state
   37.35 +  val def_i: ((Name.binding * attribute list) *
   37.36 +    ((Name.binding * mixfix) * (term * term list))) list -> state -> state
   37.37    val chain: state -> state
   37.38    val chain_facts: thm list -> state -> state
   37.39    val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   37.40 -  val note_thmss: ((string * Attrib.src list) *
   37.41 +  val note_thmss: ((Name.binding * Attrib.src list) *
   37.42      (Facts.ref * Attrib.src list) list) list -> state -> state
   37.43 -  val note_thmss_i: ((string * attribute list) *
   37.44 +  val note_thmss_i: ((Name.binding * attribute list) *
   37.45      (thm list * attribute list) list) list -> state -> state
   37.46    val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   37.47    val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   37.48 @@ -87,7 +91,7 @@
   37.49      (theory -> 'a -> attribute) ->
   37.50      (context * 'b list -> context * (term list list * (context -> context))) ->
   37.51      string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
   37.52 -    ((string * 'a list) * 'b) list -> state -> state
   37.53 +    ((Name.binding * 'a list) * 'b) list -> state -> state
   37.54    val local_qed: Method.text option * bool -> state -> state Seq.seq
   37.55    val theorem: Method.text option -> (thm list list -> context -> context) ->
   37.56      (string * string list) list list -> context -> state
   37.57 @@ -105,13 +109,13 @@
   37.58    val global_done_proof: state -> context
   37.59    val global_skip_proof: bool -> state -> context
   37.60    val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   37.61 -    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   37.62 +    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   37.63    val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   37.64 -    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   37.65 +    ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   37.66    val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   37.67 -    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   37.68 +    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   37.69    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   37.70 -    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   37.71 +    ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   37.72  end;
   37.73  
   37.74  structure Proof: PROOF =
   37.75 @@ -610,7 +614,7 @@
   37.76  
   37.77  (* note etc. *)
   37.78  
   37.79 -fun no_binding args = map (pair ("", [])) args;
   37.80 +fun no_binding args = map (pair (Name.no_binding, [])) args;
   37.81  
   37.82  local
   37.83  
   37.84 @@ -638,7 +642,7 @@
   37.85  val local_results =
   37.86    gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
   37.87  
   37.88 -fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
   37.89 +fun get_thmss state srcs = the_facts (note_thmss [((Name.no_binding, []), srcs)] state);
   37.90  
   37.91  end;
   37.92  
   37.93 @@ -682,14 +686,14 @@
   37.94      val atts = map (prep_att (theory_of state)) raw_atts;
   37.95      val (asms, state') = state |> map_context_result (fn ctxt =>
   37.96        ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
   37.97 -    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
   37.98 +    val assumptions = asms |> map (fn (a, ts) => ((Name.binding a, atts), map (rpair []) ts));
   37.99    in
  37.100      state'
  37.101      |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
  37.102      |> assume_i assumptions
  37.103      |> add_binds_i AutoBind.no_facts
  37.104      |> map_context (ProofContext.restore_naming (context_of state))
  37.105 -    |> `the_facts |-> (fn thms => note_thmss_i [((name, []), [(thms, [])])])
  37.106 +    |> `the_facts |-> (fn thms => note_thmss_i [((Name.binding name, []), [(thms, [])])])
  37.107    end;
  37.108  
  37.109  in
    38.1 --- a/src/Pure/Isar/rule_insts.ML	Tue Sep 02 14:10:32 2008 +0200
    38.2 +++ b/src/Pure/Isar/rule_insts.ML	Tue Sep 02 14:10:45 2008 +0200
    38.3 @@ -284,7 +284,7 @@
    38.4          val (param_names, ctxt') = ctxt
    38.5            |> Variable.declare_thm thm
    38.6            |> Thm.fold_terms Variable.declare_constraints st
    38.7 -          |> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params);
    38.8 +          |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params);
    38.9  
   38.10          (* Process type insts: Tinsts_env *)
   38.11          fun absent xi = error
    39.1 --- a/src/Pure/Isar/spec_parse.ML	Tue Sep 02 14:10:32 2008 +0200
    39.2 +++ b/src/Pure/Isar/spec_parse.ML	Tue Sep 02 14:10:45 2008 +0200
    39.3 @@ -11,34 +11,34 @@
    39.4    val attrib: OuterLex.token list -> Attrib.src * token list
    39.5    val attribs: token list -> Attrib.src list * token list
    39.6    val opt_attribs: token list -> Attrib.src list * token list
    39.7 -  val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    39.8 -  val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    39.9 -  val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
   39.10 -  val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
   39.11 -  val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
   39.12 -  val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
   39.13 +  val thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
   39.14 +  val opt_thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
   39.15 +  val spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
   39.16 +  val named_spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
   39.17 +  val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
   39.18 +  val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
   39.19    val xthm: token list -> (Facts.ref * Attrib.src list) * token list
   39.20    val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
   39.21    val name_facts: token list ->
   39.22 -    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
   39.23 +    ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
   39.24    val locale_mixfix: token list -> mixfix * token list
   39.25 -  val locale_fixes: token list -> (string * string option * mixfix) list * token list
   39.26 +  val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
   39.27    val locale_insts: token list ->
   39.28 -    (string option list * ((bstring * Attrib.src list) * string) list) * token list
   39.29 +    (string option list * ((Name.binding * Attrib.src list) * string) list) * token list
   39.30    val class_expr: token list -> string list * token list
   39.31    val locale_expr: token list -> Locale.expr * token list
   39.32    val locale_keyword: token list -> string * token list
   39.33    val locale_element: token list -> Element.context Locale.element * token list
   39.34    val context_element: token list -> Element.context * token list
   39.35    val statement: token list ->
   39.36 -    ((bstring * Attrib.src list) * (string * string list) list) list * token list
   39.37 +    ((Name.binding * Attrib.src list) * (string * string list) list) list * token list
   39.38    val general_statement: token list ->
   39.39      (Element.context Locale.element list * Element.statement) * OuterLex.token list
   39.40    val statement_keyword: token list -> string * token list
   39.41    val specification: token list ->
   39.42 -    (string *
   39.43 -      (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
   39.44 -    token list
   39.45 +    (Name.binding *
   39.46 +      (((Name.binding * Attrib.src list) * string list) list *
   39.47 +        (Name.binding * string option) list)) list * token list
   39.48  end;
   39.49  
   39.50  structure SpecParse: SPEC_PARSE =
   39.51 @@ -54,9 +54,11 @@
   39.52  val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
   39.53  val opt_attribs = Scan.optional attribs [];
   39.54  
   39.55 -fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
   39.56 +fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
   39.57 +
   39.58  fun opt_thm_name s =
   39.59 -  Scan.optional ((P.name -- opt_attribs || attribs >> pair "") --| P.$$$ s) ("", []);
   39.60 +  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
   39.61 +    (Name.no_binding, []);
   39.62  
   39.63  val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
   39.64  val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
   39.65 @@ -79,7 +81,7 @@
   39.66  val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
   39.67  
   39.68  val locale_fixes =
   39.69 -  P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
   39.70 +  P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
   39.71      >> (single o P.triple1) ||
   39.72    P.params >> map Syntax.no_syn) >> flat;
   39.73  
   39.74 @@ -134,7 +136,7 @@
   39.75  val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
   39.76  
   39.77  val obtain_case =
   39.78 -  P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
   39.79 +  P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
   39.80      (P.and_list1 (Scan.repeat1 P.prop) >> flat));
   39.81  
   39.82  val general_statement =
   39.83 @@ -148,6 +150,6 @@
   39.84  
   39.85  (* specifications *)
   39.86  
   39.87 -val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes));
   39.88 +val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
   39.89  
   39.90  end;
    40.1 --- a/src/Pure/Isar/theory_target.ML	Tue Sep 02 14:10:32 2008 +0200
    40.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Sep 02 14:10:45 2008 +0200
    40.3 @@ -48,8 +48,10 @@
    40.4    let
    40.5      val thy = ProofContext.theory_of ctxt;
    40.6      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    40.7 -    val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
    40.8 -    val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
    40.9 +    val fixes = map (fn (x, T) =>
   40.10 +      (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
   40.11 +    val assumes = map (fn A =>
   40.12 +      ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
   40.13      val elems =
   40.14        (if null fixes then [] else [Element.Fixes fixes]) @
   40.15        (if null assumes then [] else [Element.Assumes assumes]);
   40.16 @@ -118,7 +120,7 @@
   40.17        |> Drule.zero_var_indexes_list;
   40.18  
   40.19      (*thm definition*)
   40.20 -    val result = PureThy.name_thm true true name th'';
   40.21 +    val result = PureThy.name_thm true true Position.none name th'';
   40.22  
   40.23      (*import fixes*)
   40.24      val (tvars, vars) =
   40.25 @@ -138,7 +140,7 @@
   40.26          NONE => raise THM ("Failed to re-import result", 0, [result'])
   40.27        | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
   40.28        |> Goal.norm_result
   40.29 -      |> PureThy.name_thm false false name;
   40.30 +      |> PureThy.name_thm false false Position.none name;
   40.31  
   40.32    in (result'', result) end;
   40.33  
   40.34 @@ -154,7 +156,8 @@
   40.35      val full = LocalTheory.full_name lthy;
   40.36  
   40.37      val facts' = facts
   40.38 -      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (full (fst a))) bs))
   40.39 +      |> map (fn (a, bs) =>
   40.40 +        (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs))
   40.41        |> PureThy.map_facts (import_export_proof lthy);
   40.42      val local_facts = PureThy.map_facts #1 facts'
   40.43        |> Attrib.map_facts (Attrib.attribute_i thy);
   40.44 @@ -185,11 +188,13 @@
   40.45    let
   40.46      val c' = Morphism.name phi c;
   40.47      val rhs' = Morphism.term phi rhs;
   40.48 -    val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
   40.49 -    val arg = (c', Term.close_schematic_term rhs');
   40.50 +    val name = Name.name_of c;
   40.51 +    val name' = Name.name_of c'
   40.52 +    val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
   40.53 +    val arg = (name', Term.close_schematic_term rhs');
   40.54      val similar_body = Type.similar_types (rhs, rhs');
   40.55      (* FIXME workaround based on educated guess *)
   40.56 -    val class_global = c' = NameSpace.qualified (Class.class_prefix target) c;
   40.57 +    val class_global = name' = NameSpace.qualified (Class.class_prefix target) name;
   40.58    in
   40.59      not (is_class andalso (similar_body orelse class_global)) ?
   40.60        (Context.mapping_result
   40.61 @@ -201,8 +206,9 @@
   40.62               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   40.63    end;
   40.64  
   40.65 -fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
   40.66 +fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   40.67    let
   40.68 +    val c = Name.name_of b;
   40.69      val tags = LocalTheory.group_position_of lthy;
   40.70      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   40.71      val U = map #2 xs ---> T;
   40.72 @@ -225,16 +231,17 @@
   40.73      val t = Term.list_comb (const, map Free xs);
   40.74    in
   40.75      lthy'
   40.76 -    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((c, mx2), t))
   40.77 +    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
   40.78      |> is_class ? class_target ta (Class.declare target tags ((c, mx1), t))
   40.79 -    |> LocalDefs.add_def ((c, NoSyn), t)
   40.80 +    |> LocalDefs.add_def ((b, NoSyn), t)
   40.81    end;
   40.82  
   40.83  
   40.84  (* abbrev *)
   40.85  
   40.86 -fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
   40.87 +fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   40.88    let
   40.89 +    val c = Name.name_of b;
   40.90      val tags = LocalTheory.group_position_of lthy;
   40.91      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   40.92      val target_ctxt = LocalTheory.target_of lthy;
   40.93 @@ -251,7 +258,7 @@
   40.94          LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
   40.95          #-> (fn (lhs, _) =>
   40.96            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
   40.97 -            term_syntax ta (locale_const ta prmode tags ((c, mx2), lhs')) #>
   40.98 +            term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
   40.99              is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t'))
  40.100            end)
  40.101        else
  40.102 @@ -259,26 +266,27 @@
  40.103            (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
  40.104             Sign.notation true prmode [(lhs, mx3)])))
  40.105      |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
  40.106 -    |> LocalDefs.fixed_abbrev ((c, NoSyn), t)
  40.107 +    |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
  40.108    end;
  40.109  
  40.110  
  40.111  (* define *)
  40.112  
  40.113  fun define (ta as Target {target, is_locale, is_class, ...})
  40.114 -    kind ((c, mx), ((name, atts), rhs)) lthy =
  40.115 +    kind ((b, mx), ((name, atts), rhs)) lthy =
  40.116    let
  40.117      val thy = ProofContext.theory_of lthy;
  40.118      val thy_ctxt = ProofContext.init thy;
  40.119  
  40.120 -    val name' = Thm.def_name_optional c name;
  40.121 +    val c = Name.name_of b;
  40.122 +    val name' = Name.map_name (Thm.def_name_optional c) name;
  40.123      val (rhs', rhs_conv) =
  40.124        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
  40.125      val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
  40.126      val T = Term.fastype_of rhs;
  40.127  
  40.128      (*const*)
  40.129 -    val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((c, T), mx);
  40.130 +    val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((b, T), mx);
  40.131      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
  40.132  
  40.133      (*def*)
  40.134 @@ -291,7 +299,7 @@
  40.135            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
  40.136            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
  40.137      val (global_def, lthy3) = lthy2
  40.138 -      |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
  40.139 +      |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
  40.140      val def = LocalDefs.trans_terms lthy3
  40.141        [(*c == global.c xs*)     local_def,
  40.142         (*global.c xs == rhs'*)  global_def,
  40.143 @@ -318,7 +326,7 @@
  40.144      (*axioms*)
  40.145      val hyps = map Thm.term_of (Assumption.assms_of lthy');
  40.146      fun axiom ((name, atts), props) thy = thy
  40.147 -      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
  40.148 +      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi (Name.name_of name) props)
  40.149        |-> (fn ths => pair ((name, atts), [(ths, [])]));
  40.150    in
  40.151      lthy'
    41.1 --- a/src/Pure/Tools/invoke.ML	Tue Sep 02 14:10:32 2008 +0200
    41.2 +++ b/src/Pure/Tools/invoke.ML	Tue Sep 02 14:10:45 2008 +0200
    41.3 @@ -8,9 +8,9 @@
    41.4  signature INVOKE =
    41.5  sig
    41.6    val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
    41.7 -    (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    41.8 +    (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    41.9    val invoke_i: string * attribute list -> Locale.expr -> term option list ->
   41.10 -    (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   41.11 +    (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   41.12  end;
   41.13  
   41.14  structure Invoke: INVOKE =
   41.15 @@ -60,9 +60,9 @@
   41.16          | NONE => Drule.termI)) params';
   41.17  
   41.18      val propp =
   41.19 -      [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
   41.20 -       (("", []), map (rpair [] o Logic.mk_term) params'),
   41.21 -       (("", []), map (rpair [] o Element.mark_witness) prems')];
   41.22 +      [((Name.no_binding, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
   41.23 +       ((Name.no_binding, []), map (rpair [] o Logic.mk_term) params'),
   41.24 +       ((Name.no_binding, []), map (rpair [] o Element.mark_witness) prems')];
   41.25      fun after_qed results =
   41.26        Proof.end_block #>
   41.27        Proof.map_context (fn ctxt =>
   41.28 @@ -120,8 +120,8 @@
   41.29      "schematic invocation of locale expression in proof context"
   41.30      (K.tag_proof K.prf_goal)
   41.31      (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
   41.32 -      >> (fn (((name, expr), (insts, _)), fixes) =>
   41.33 -          Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
   41.34 +      >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
   41.35 +          Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
   41.36  
   41.37  end;
   41.38  
    42.1 --- a/src/Pure/axclass.ML	Tue Sep 02 14:10:32 2008 +0200
    42.2 +++ b/src/Pure/axclass.ML	Tue Sep 02 14:10:45 2008 +0200
    42.3 @@ -9,7 +9,7 @@
    42.4  signature AX_CLASS =
    42.5  sig
    42.6    val define_class: bstring * class list -> string list ->
    42.7 -    ((bstring * attribute list) * term list) list -> theory -> class * theory
    42.8 +    ((Name.binding * attribute list) * term list) list -> theory -> class * theory
    42.9    val add_classrel: thm -> theory -> theory
   42.10    val add_arity: thm -> theory -> theory
   42.11    val prove_classrel: class * class -> tactic -> theory -> theory
   42.12 @@ -482,9 +482,10 @@
   42.13        |> Sign.add_path bconst
   42.14        |> Sign.no_base_names
   42.15        |> PureThy.note_thmss ""
   42.16 -        [((introN, []), [([Drule.standard raw_intro], [])]),
   42.17 -         ((superN, []), [(map Drule.standard raw_classrel, [])]),
   42.18 -         ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
   42.19 +        [((Name.binding introN, []), [([Drule.standard raw_intro], [])]),
   42.20 +         ((Name.binding superN, []), [(map Drule.standard raw_classrel, [])]),
   42.21 +         ((Name.binding axiomsN, []),
   42.22 +           [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
   42.23        ||> Sign.restore_naming def_thy;
   42.24  
   42.25  
    43.1 --- a/src/Tools/induct.ML	Tue Sep 02 14:10:32 2008 +0200
    43.2 +++ b/src/Tools/induct.ML	Tue Sep 02 14:10:45 2008 +0200
    43.3 @@ -51,7 +51,7 @@
    43.4    val setN: string
    43.5    (*proof methods*)
    43.6    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    43.7 -  val add_defs: (string option * term) option list -> Proof.context ->
    43.8 +  val add_defs: (Name.binding option * term) option list -> Proof.context ->
    43.9      (term option list * thm list) * Proof.context
   43.10    val atomize_term: theory -> term -> term
   43.11    val atomize_tac: int -> tactic
   43.12 @@ -63,7 +63,7 @@
   43.13    val cases_tac: Proof.context -> term option list list -> thm option ->
   43.14      thm list -> int -> cases_tactic
   43.15    val get_inductT: Proof.context -> term option list list -> thm list list
   43.16 -  val induct_tac: Proof.context -> (string option * term) option list list ->
   43.17 +  val induct_tac: Proof.context -> (Name.binding option * term) option list list ->
   43.18      (string * typ) list list -> term option list -> thm list option ->
   43.19      thm list -> int -> cases_tactic
   43.20    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
   43.21 @@ -552,7 +552,8 @@
   43.22  fun add_defs def_insts =
   43.23    let
   43.24      fun add (SOME (SOME x, t)) ctxt =
   43.25 -          let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
   43.26 +          let val ([(lhs, (_, th))], ctxt') =
   43.27 +            LocalDefs.add_defs [((x, NoSyn), ((Name.no_binding, []), t))] ctxt
   43.28            in ((SOME lhs, [th]), ctxt') end
   43.29        | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
   43.30        | add NONE ctxt = ((NONE, []), ctxt);
   43.31 @@ -716,7 +717,7 @@
   43.32  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
   43.33  
   43.34  val def_inst =
   43.35 -  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
   43.36 +  ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
   43.37        -- Args.term) >> SOME ||
   43.38      inst >> Option.map (pair NONE);
   43.39  
    44.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Sep 02 14:10:32 2008 +0200
    44.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Sep 02 14:10:45 2008 +0200
    44.3 @@ -262,7 +262,7 @@
    44.4               ||> add_recursor
    44.5               ||> Sign.parent_path
    44.6  
    44.7 -  val intr_names = map #2 (List.concat con_ty_lists);
    44.8 +  val intr_names = map (Name.binding o #2) (List.concat con_ty_lists);
    44.9    val (thy1, ind_result) =
   44.10      thy0 |> Ind_Package.add_inductive_i
   44.11        false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
    45.1 --- a/src/ZF/Tools/ind_cases.ML	Tue Sep 02 14:10:32 2008 +0200
    45.2 +++ b/src/ZF/Tools/ind_cases.ML	Tue Sep 02 14:10:45 2008 +0200
    45.3 @@ -8,7 +8,7 @@
    45.4  signature IND_CASES =
    45.5  sig
    45.6    val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
    45.7 -  val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    45.8 +  val inductive_cases: ((Name.binding * Attrib.src list) * string list) list -> theory -> theory
    45.9    val setup: theory -> theory
   45.10  end;
   45.11  
    46.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Sep 02 14:10:32 2008 +0200
    46.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 02 14:10:45 2008 +0200
    46.3 @@ -29,10 +29,10 @@
    46.4    (*Insert definitions for the recursive sets, which
    46.5       must *already* be declared as constants in parent theory!*)
    46.6    val add_inductive_i: bool -> term list * term ->
    46.7 -    ((bstring * term) * attribute list) list ->
    46.8 +    ((Name.binding * term) * attribute list) list ->
    46.9      thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   46.10    val add_inductive: string list * string ->
   46.11 -    ((bstring * string) * Attrib.src list) list ->
   46.12 +    ((Name.binding * string) * Attrib.src list) list ->
   46.13      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
   46.14      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
   46.15      theory -> theory * inductive_result
   46.16 @@ -62,11 +62,12 @@
   46.17  
   46.18  (*internal version, accepting terms*)
   46.19  fun add_inductive_i verbose (rec_tms, dom_sum)
   46.20 -  intr_specs (monos, con_defs, type_intrs, type_elims) thy =
   46.21 +  raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
   46.22  let
   46.23    val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
   46.24    val ctxt = ProofContext.init thy;
   46.25  
   46.26 +  val intr_specs = map (apfst (apfst Name.name_of)) raw_intr_specs;
   46.27    val (intr_names, intr_tms) = split_list (map fst intr_specs);
   46.28    val case_names = RuleCases.case_names intr_names;
   46.29  
    47.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Sep 02 14:10:32 2008 +0200
    47.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Sep 02 14:10:45 2008 +0200
    47.3 @@ -9,8 +9,8 @@
    47.4  
    47.5  signature PRIMREC_PACKAGE =
    47.6  sig
    47.7 -  val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
    47.8 -  val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
    47.9 +  val add_primrec: ((Name.binding * string) * Attrib.src list) list -> theory -> theory * thm list
   47.10 +  val add_primrec_i: ((Name.binding * term) * attribute list) list -> theory -> theory * thm list
   47.11  end;
   47.12  
   47.13  structure PrimrecPackage : PRIMREC_PACKAGE =
   47.14 @@ -180,7 +180,7 @@
   47.15  
   47.16      val (eqn_thms', thy2) =
   47.17        thy1
   47.18 -      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   47.19 +      |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
   47.20      val (_, thy3) =
   47.21        thy2
   47.22        |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]