1.1 --- a/NEWS	Fri Jun 27 15:41:26 2014 +0200
     1.2 +++ b/NEWS	Fri Jun 27 16:04:56 2014 +0200
     1.3 @@ -205,6 +205,9 @@
     1.4  (only makes sense in practice, if outer syntax is delimited
     1.5  differently).
     1.6  
     1.7 +* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
     1.8 +but the latter is retained some time as Proof General legacy.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  

     2.1 --- a/etc/isar-keywords-ZF.el	Fri Jun 27 15:41:26 2014 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Fri Jun 27 16:04:56 2014 +0200
     2.3 @@ -147,6 +147,7 @@
     2.4      "print_statement"
     2.5      "print_syntax"
     2.6      "print_tcset"
     2.7 +    "print_term_bindings"
     2.8      "print_theorems"
     2.9      "print_theory"
    2.10      "print_trans_rules"
    2.11 @@ -316,6 +317,7 @@
    2.12      "print_statement"
    2.13      "print_syntax"
    2.14      "print_tcset"
    2.15 +    "print_term_bindings"
    2.16      "print_theorems"
    2.17      "print_theory"
    2.18      "print_trans_rules"

     3.1 --- a/etc/isar-keywords.el	Fri Jun 27 15:41:26 2014 +0200
     3.2 +++ b/etc/isar-keywords.el	Fri Jun 27 16:04:56 2014 +0200
     3.3 @@ -213,6 +213,7 @@
     3.4      "print_state"
     3.5      "print_statement"
     3.6      "print_syntax"
     3.7 +    "print_term_bindings"
     3.8      "print_theorems"
     3.9      "print_theory"
    3.10      "print_trans_rules"
    3.11 @@ -445,6 +446,7 @@
    3.12      "print_state"
    3.13      "print_statement"
    3.14      "print_syntax"
    3.15 +    "print_term_bindings"
    3.16      "print_theorems"
    3.17      "print_theory"
    3.18      "print_trans_rules"

     4.1 --- a/src/Doc/Isar_Ref/Misc.thy	Fri Jun 27 15:41:26 2014 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Misc.thy	Fri Jun 27 16:04:56 2014 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4      @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.5      @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.6      @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.7 -    @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.8 +    @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.9    \end{matharray}
    4.10  
    4.11    @{rail \<open>
    4.12 @@ -63,8 +63,8 @@
    4.13    current context, both named and unnamed ones; the ``@{text "!"}''
    4.14    option indicates extra verbosity.
    4.15    
    4.16 -  \item @{command "print_binds"} prints all term abbreviations
    4.17 -  present in the context.
    4.18 +  \item @{command "print_term_bindings"} prints all term bindings that
    4.19 +  are present in the context.
    4.20  
    4.21    \item @{command "find_theorems"}~@{text criteria} retrieves facts
    4.22    from the theory or proof context matching all of given search

     5.1 --- a/src/Doc/JEdit/JEdit.thy	Fri Jun 27 15:41:26 2014 +0200
     5.2 +++ b/src/Doc/JEdit/JEdit.thy	Fri Jun 27 16:04:56 2014 +0200
     5.3 @@ -960,8 +960,8 @@
     5.4    The \emph{Query} panel in \emph{Print Context} mode prints information from
     5.5    the theory or proof context, or proof state. See also the Isar commands
     5.6    @{command_ref print_context}, @{command_ref print_cases}, @{command_ref
     5.7 -  print_binds}, @{command_ref print_theorems}, @{command_ref print_state} in
     5.8 -  \cite{isabelle-isar-ref}.
     5.9 +  print_term_bindings}, @{command_ref print_theorems},
    5.10 +  @{command_ref print_state} in \cite{isabelle-isar-ref}.
    5.11  *}
    5.12  
    5.13  

     6.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jun 27 15:41:26 2014 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 27 16:04:56 2014 +0200
     6.3 @@ -897,9 +897,18 @@
     6.4      (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
     6.8 +  Outer_Syntax.improper_command @{command_spec "print_binds"}
     6.9 +    "print term bindings of proof context -- Proof General legacy"
    6.10      (Scan.succeed (Toplevel.unknown_context o
    6.11 -      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_binds o Toplevel.context_of)));
    6.12 +      Toplevel.keep
    6.13 +        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
    6.14 +
    6.15 +val _ =
    6.16 +  Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
    6.17 +    "print term bindings of proof context"
    6.18 +    (Scan.succeed (Toplevel.unknown_context o
    6.19 +      Toplevel.keep
    6.20 +        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
    6.21  
    6.22  val _ =
    6.23    Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"

     7.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jun 27 15:41:26 2014 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jun 27 16:04:56 2014 +0200
     7.3 @@ -161,7 +161,7 @@
     7.4    val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
     7.5    val print_syntax: Proof.context -> unit
     7.6    val print_abbrevs: Proof.context -> unit
     7.7 -  val pretty_binds: Proof.context -> Pretty.T list
     7.8 +  val pretty_term_bindings: Proof.context -> Pretty.T list
     7.9    val pretty_local_facts: Proof.context -> bool -> Pretty.T list
    7.10    val print_local_facts: Proof.context -> bool -> unit
    7.11    val pretty_cases: Proof.context -> Pretty.T list
    7.12 @@ -1257,7 +1257,7 @@
    7.13  
    7.14  (* term bindings *)
    7.15  
    7.16 -fun pretty_binds ctxt =
    7.17 +fun pretty_term_bindings ctxt =
    7.18    let
    7.19      val binds = Variable.binds_of ctxt;
    7.20      fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t));
    7.21 @@ -1408,7 +1408,7 @@
    7.22      verb single (K pretty_thy) @
    7.23      pretty_ctxt ctxt @
    7.24      verb (pretty_abbrevs false) (K ctxt) @
    7.25 -    verb pretty_binds (K ctxt) @
    7.26 +    verb pretty_term_bindings (K ctxt) @
    7.27      verb (pretty_local_facts ctxt) (K true) @
    7.28      verb pretty_cases (K ctxt) @
    7.29      verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @

     8.1 --- a/src/Pure/Pure.thy	Fri Jun 27 15:41:26 2014 +0200
     8.2 +++ b/src/Pure/Pure.thy	Fri Jun 27 16:04:56 2014 +0200
     8.3 @@ -85,10 +85,9 @@
     8.4      "print_interps" "print_dependencies" "print_attributes"
     8.5      "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     8.6      "print_antiquotations" "print_ML_antiquotations" "thy_deps"
     8.7 -    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_facts"
     8.8 -    "print_cases" "print_statement" "thm" "prf" "full_prf" "prop"
     8.9 -    "term" "typ" "print_codesetup" "unused_thms"
    8.10 -    :: diag
    8.11 +    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
    8.12 +    "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
    8.13 +    "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
    8.14    and "cd" :: control
    8.15    and "pwd" :: diag
    8.16    and "use_thy" "remove_thy" "kill_thy" :: control

     9.1 --- a/src/Pure/Tools/print_operation.ML	Fri Jun 27 15:41:26 2014 +0200
     9.2 +++ b/src/Pure/Tools/print_operation.ML	Fri Jun 27 16:04:56 2014 +0200
     9.3 @@ -70,7 +70,7 @@
     9.4  
     9.5  val _ =
     9.6    register "terms" "term bindings of proof context"
     9.7 -    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
     9.8 +    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of);
     9.9  
    9.10  val _ =
    9.11    register "theorems" "theorems of local theory or proof context"