src/Pure/Isar/proof_context.ML
changeset 25052 a014d544f54d
parent 25039 06ed511837d5
child 25060 17c313217998
equal deleted inserted replaced
25051:71cd45fdf332 25052:a014d544f54d
   142   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
   142   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
   143     Context.generic -> Context.generic
   143     Context.generic -> Context.generic
   144   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   144   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   145   val add_abbrev: string -> Markup.property list ->
   145   val add_abbrev: string -> Markup.property list ->
   146     bstring * term -> Proof.context -> (term * term) * Proof.context
   146     bstring * term -> Proof.context -> (term * term) * Proof.context
       
   147   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   147   val verbose: bool ref
   148   val verbose: bool ref
   148   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   149   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   149   val print_syntax: Proof.context -> unit
   150   val print_syntax: Proof.context -> unit
   150   val print_abbrevs: Proof.context -> unit
   151   val print_abbrevs: Proof.context -> unit
   151   val print_binds: Proof.context -> unit
   152   val print_binds: Proof.context -> unit
   257 val syntax_of = #syntax o rep_context;
   258 val syntax_of = #syntax o rep_context;
   258 val syn_of = LocalSyntax.syn_of o syntax_of;
   259 val syn_of = LocalSyntax.syn_of o syntax_of;
   259 val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
   260 val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
   260 val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
   261 val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
   261 
   262 
   262 val consts_of = fst o #consts o rep_context;
   263 val consts_of = #1 o #consts o rep_context;
   263 val const_syntax_name = Consts.syntax_name o consts_of;
   264 val const_syntax_name = Consts.syntax_name o consts_of;
   264 val the_const_constraint = Consts.the_constraint o consts_of;
   265 val the_const_constraint = Consts.the_constraint o consts_of;
   265 
   266 
   266 val thms_of = #thms o rep_context;
   267 val thms_of = #thms o rep_context;
   267 val theorems_of = #1 o thms_of;
   268 val theorems_of = #1 o thms_of;
   427   let
   428   let
   428     val thy = theory_of ctxt;
   429     val thy = theory_of ctxt;
   429     val consts = consts_of ctxt;
   430     val consts = consts_of ctxt;
   430     val Mode {abbrev, ...} = get_mode ctxt;
   431     val Mode {abbrev, ...} = get_mode ctxt;
   431   in
   432   in
   432     if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t)
   433     if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
   433     then t
   434     else t |> Pattern.rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) []
   434     else
       
   435       t
       
   436       |> Pattern.rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) []
       
   437       |> Pattern.rewrite_term thy (Consts.abbrevs_of consts [Syntax.internalM]) []
       
   438   end;
   435   end;
   439 
   436 
   440 
   437 
   441 (* patterns *)
   438 (* patterns *)
   442 
   439 
  1040     |> (map_consts o apfst) (K consts')
  1037     |> (map_consts o apfst) (K consts')
  1041     |> Variable.declare_term rhs
  1038     |> Variable.declare_term rhs
  1042     |> pair (lhs, rhs)
  1039     |> pair (lhs, rhs)
  1043   end;
  1040   end;
  1044 
  1041 
       
  1042 fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
       
  1043 
  1045 
  1044 
  1046 (* fixes *)
  1045 (* fixes *)
  1047 
  1046 
  1048 local
  1047 local
  1049 
  1048 
  1193 
  1192 
  1194 (* abbreviations *)
  1193 (* abbreviations *)
  1195 
  1194 
  1196 fun pretty_abbrevs show_globals ctxt =
  1195 fun pretty_abbrevs show_globals ctxt =
  1197   let
  1196   let
  1198     val ((_, globals), (space, consts)) =
  1197     val ((space, consts), (_, globals)) =
  1199       pairself (#constants o Consts.dest) (#consts (rep_context ctxt));
  1198       pairself (#constants o Consts.dest) (#consts (rep_context ctxt));
  1200     fun add_abbr (_, (_, NONE)) = I
  1199     fun add_abbr (_, (_, NONE)) = I
  1201       | add_abbr (c, (T, SOME (t, _))) =
  1200       | add_abbr (c, (T, SOME (t, _))) =
  1202           if not show_globals andalso Symtab.defined globals c then I
  1201           if not show_globals andalso Symtab.defined globals c then I
  1203           else cons (c, Logic.mk_equals (Const (c, T), t));
  1202           else cons (c, Logic.mk_equals (Const (c, T), t));