src/Pure/Isar/proof_context.ML
changeset 28965 1de908189869
parent 28941 128459bd72d2
child 29006 abe0f11cfa4e
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -23,8 +23,8 @@
     1.4    val abbrev_mode: Proof.context -> bool
     1.5    val set_stmt: bool -> Proof.context -> Proof.context
     1.6    val naming_of: Proof.context -> NameSpace.naming
     1.7 -  val full_name: Proof.context -> bstring -> string
     1.8 -  val full_binding: Proof.context -> Name.binding -> string
     1.9 +  val full_name: Proof.context -> Binding.T -> string
    1.10 +  val full_bname: Proof.context -> bstring -> string
    1.11    val consts_of: Proof.context -> Consts.T
    1.12    val const_syntax_name: Proof.context -> string -> string
    1.13    val the_const_constraint: Proof.context -> string -> typ
    1.14 @@ -105,27 +105,27 @@
    1.15    val restore_naming: Proof.context -> Proof.context -> Proof.context
    1.16    val reset_naming: Proof.context -> Proof.context
    1.17    val note_thmss: string ->
    1.18 -    ((Name.binding * attribute list) * (Facts.ref * attribute list) list) list ->
    1.19 +    ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list ->
    1.20        Proof.context -> (string * thm list) list * Proof.context
    1.21    val note_thmss_i: string ->
    1.22 -    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    1.23 +    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
    1.24        Proof.context -> (string * thm list) list * Proof.context
    1.25    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
    1.26 -  val read_vars: (Name.binding * string option * mixfix) list -> Proof.context ->
    1.27 -    (Name.binding * typ option * mixfix) list * Proof.context
    1.28 -  val cert_vars: (Name.binding * typ option * mixfix) list -> Proof.context ->
    1.29 -    (Name.binding * typ option * mixfix) list * Proof.context
    1.30 -  val add_fixes: (Name.binding * string option * mixfix) list ->
    1.31 +  val read_vars: (Binding.T * string option * mixfix) list -> Proof.context ->
    1.32 +    (Binding.T * typ option * mixfix) list * Proof.context
    1.33 +  val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context ->
    1.34 +    (Binding.T * typ option * mixfix) list * Proof.context
    1.35 +  val add_fixes: (Binding.T * string option * mixfix) list ->
    1.36      Proof.context -> string list * Proof.context
    1.37 -  val add_fixes_i: (Name.binding * typ option * mixfix) list ->
    1.38 +  val add_fixes_i: (Binding.T * typ option * mixfix) list ->
    1.39      Proof.context -> string list * Proof.context
    1.40    val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
    1.41    val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
    1.42    val add_assms: Assumption.export ->
    1.43 -    ((Name.binding * attribute list) * (string * string list) list) list ->
    1.44 +    ((Binding.T * attribute list) * (string * string list) list) list ->
    1.45      Proof.context -> (string * thm list) list * Proof.context
    1.46    val add_assms_i: Assumption.export ->
    1.47 -    ((Name.binding * attribute list) * (term * term list) list) list ->
    1.48 +    ((Binding.T * attribute list) * (term * term list) list) list ->
    1.49      Proof.context -> (string * thm list) list * Proof.context
    1.50    val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
    1.51    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
    1.52 @@ -135,7 +135,7 @@
    1.53      Context.generic -> Context.generic
    1.54    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
    1.55    val add_abbrev: string -> Properties.T ->
    1.56 -    Name.binding * term -> Proof.context -> (term * term) * Proof.context
    1.57 +    Binding.T * term -> Proof.context -> (term * term) * Proof.context
    1.58    val revert_abbrev: string -> string -> Proof.context -> Proof.context
    1.59    val verbose: bool ref
    1.60    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    1.61 @@ -247,8 +247,8 @@
    1.62  
    1.63  val naming_of = #naming o rep_context;
    1.64  
    1.65 -val full_name = NameSpace.full o naming_of;
    1.66 -val full_binding = NameSpace.full_binding o naming_of;
    1.67 +val full_name = NameSpace.full_name o naming_of;
    1.68 +fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
    1.69  
    1.70  val syntax_of = #syntax o rep_context;
    1.71  val syn_of = LocalSyntax.syn_of o syntax_of;
    1.72 @@ -965,14 +965,14 @@
    1.73  
    1.74  local
    1.75  
    1.76 -fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
    1.77 +fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
    1.78    | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
    1.79        (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
    1.80  
    1.81  fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
    1.82    let
    1.83      val pos = Binding.pos_of b;
    1.84 -    val name = full_binding ctxt b;
    1.85 +    val name = full_name ctxt b;
    1.86      val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
    1.87  
    1.88      val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
    1.89 @@ -991,7 +991,7 @@
    1.90  fun put_thms do_props thms ctxt = ctxt
    1.91    |> map_naming (K local_naming)
    1.92    |> ContextPosition.set_visible false
    1.93 -  |> update_thms do_props (apfst Name.binding thms)
    1.94 +  |> update_thms do_props (apfst Binding.name thms)
    1.95    |> ContextPosition.restore_visible ctxt
    1.96    |> restore_naming ctxt;
    1.97  
    1.98 @@ -1021,7 +1021,7 @@
    1.99          if internal then T
   1.100          else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
   1.101        val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
   1.102 -      val var = (Name.map_name (K x) raw_b, opt_T, mx);
   1.103 +      val var = (Binding.map_base (K x) raw_b, opt_T, mx);
   1.104      in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
   1.105  
   1.106  in
   1.107 @@ -1095,7 +1095,7 @@
   1.108  fun add_abbrev mode tags (b, raw_t) ctxt =
   1.109    let
   1.110      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
   1.111 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
   1.112 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
   1.113      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
   1.114      val ((lhs, rhs), consts') = consts_of ctxt
   1.115        |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
   1.116 @@ -1146,7 +1146,7 @@
   1.117  
   1.118  fun bind_fixes xs ctxt =
   1.119    let
   1.120 -    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Name.binding x, NONE, NoSyn)) xs);
   1.121 +    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
   1.122      fun bind (t as Free (x, T)) =
   1.123            if member (op =) xs x then
   1.124              (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)