src/Pure/Isar/proof_context.ML
changeset 28861 f53abb0733ee
parent 28856 5e009a80fe6d
child 28864 d6fe93e3dcb9
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Nov 20 14:51:40 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Nov 20 14:55:25 2008 +0100
     1.3 @@ -26,6 +26,7 @@
     1.4    val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context)
     1.5      -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context
     1.6    val full_name: Proof.context -> bstring -> string
     1.7 +  val full_binding: Proof.context -> Name.binding -> string
     1.8    val consts_of: Proof.context -> Consts.T
     1.9    val const_syntax_name: Proof.context -> string -> string
    1.10    val the_const_constraint: Proof.context -> string -> typ
    1.11 @@ -136,7 +137,7 @@
    1.12      Context.generic -> Context.generic
    1.13    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
    1.14    val add_abbrev: string -> Properties.T ->
    1.15 -    bstring * term -> Proof.context -> (term * term) * Proof.context
    1.16 +    Name.binding * term -> Proof.context -> (term * term) * Proof.context
    1.17    val revert_abbrev: string -> string -> Proof.context -> Proof.context
    1.18    val verbose: bool ref
    1.19    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    1.20 @@ -248,19 +249,20 @@
    1.21  
    1.22  val naming_of = #naming o rep_context;
    1.23  
    1.24 -fun name_decl decl (binding, x) ctxt =
    1.25 +fun name_decl decl (b, x) ctxt =
    1.26    let
    1.27      val naming = naming_of ctxt;
    1.28 -    val (naming', name) = Name.namify naming binding;
    1.29 +    val (naming', name) = Name.namify naming b;
    1.30    in
    1.31      ctxt
    1.32      |> map_naming (K naming')
    1.33 -    |> decl (Name.name_of binding, x)
    1.34 +    |> decl (Name.name_of b, x)
    1.35      |>> pair name
    1.36      ||> map_naming (K naming)
    1.37    end;
    1.38  
    1.39  val full_name = NameSpace.full o naming_of;
    1.40 +val full_binding = NameSpace.full_binding o naming_of;
    1.41  
    1.42  val syntax_of = #syntax o rep_context;
    1.43  val syn_of = LocalSyntax.syn_of o syntax_of;
    1.44 @@ -977,15 +979,14 @@
    1.45  
    1.46  local
    1.47  
    1.48 -fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname))
    1.49 -  | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts
    1.50 -      (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths));
    1.51 +fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
    1.52 +  | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
    1.53 +      (Facts.add_local do_props (naming_of ctxt) (full_binding ctxt b, ths));
    1.54  
    1.55 -fun gen_note_thmss get k = fold_map (fn ((binding, more_attrs), raw_facts) => fn ctxt =>
    1.56 +fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
    1.57    let
    1.58 -    val bname = Name.name_of binding;
    1.59 -    val pos = Name.pos_of binding;
    1.60 -    val name = full_name ctxt bname;
    1.61 +    val pos = Name.pos_of b;
    1.62 +    val name = full_binding ctxt b;
    1.63      val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
    1.64  
    1.65      val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
    1.66 @@ -994,7 +995,7 @@
    1.67      val (res, ctxt') = fold_map app facts ctxt;
    1.68      val thms = PureThy.name_thms false false pos name (flat res);
    1.69      val Mode {stmt, ...} = get_mode ctxt;
    1.70 -  in ((name, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end);
    1.71 +  in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
    1.72  
    1.73  in
    1.74  
    1.75 @@ -1004,7 +1005,7 @@
    1.76  fun put_thms do_props thms ctxt = ctxt
    1.77    |> map_naming (K local_naming)
    1.78    |> ContextPosition.set_visible false
    1.79 -  |> update_thms do_props thms
    1.80 +  |> update_thms do_props (apfst Name.binding thms)
    1.81    |> ContextPosition.restore_visible ctxt
    1.82    |> restore_naming ctxt;
    1.83  
    1.84 @@ -1023,9 +1024,9 @@
    1.85  local
    1.86  
    1.87  fun prep_vars prep_typ internal =
    1.88 -  fold_map (fn (raw_binding, raw_T, raw_mx) => fn ctxt =>
    1.89 +  fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
    1.90      let
    1.91 -      val raw_x = Name.name_of raw_binding;
    1.92 +      val raw_x = Name.name_of raw_b;
    1.93        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
    1.94        val _ = Syntax.is_identifier (no_skolem internal x) orelse
    1.95          error ("Illegal variable name: " ^ quote x);
    1.96 @@ -1034,7 +1035,7 @@
    1.97          if internal then T
    1.98          else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
    1.99        val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
   1.100 -      val var = (Name.map_name (K x) raw_binding, opt_T, mx);
   1.101 +      val var = (Name.map_name (K x) raw_b, opt_T, mx);
   1.102      in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
   1.103  
   1.104  in
   1.105 @@ -1105,13 +1106,13 @@
   1.106        in cert_term ctxt (Const (c, T)); T end;
   1.107    in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
   1.108  
   1.109 -fun add_abbrev mode tags (c, raw_t) ctxt =
   1.110 +fun add_abbrev mode tags (b, raw_t) ctxt =
   1.111    let
   1.112      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
   1.113 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   1.114 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
   1.115      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
   1.116      val ((lhs, rhs), consts') = consts_of ctxt
   1.117 -      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t);
   1.118 +      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
   1.119    in
   1.120      ctxt
   1.121      |> (map_consts o apfst) (K consts')
   1.122 @@ -1140,8 +1141,8 @@
   1.123        ctxt'
   1.124        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
   1.125        |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
   1.126 -    val _ = (vars ~~ xs') |> List.app (fn ((binding, _, _), x') =>
   1.127 -      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of binding));
   1.128 +    val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
   1.129 +      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b));
   1.130    in (xs', ctxt'') end;
   1.131  
   1.132  in