clarified print_local_facts;
authorwenzelm
Sat Mar 15 10:14:42 2014 +0100 (2014-03-15)
changeset 561551b9c089ed12d
parent 56154 f0a927235162
child 56156 47015872e795
clarified print_local_facts;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 08:31:33 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 10:14:42 2014 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4  (* print theorems *)
     1.5  
     1.6  val print_theorems_proof =
     1.7 -  Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);
     1.8 +  Toplevel.keep (Proof_Context.print_local_facts o Proof.context_of o Toplevel.proof_of);
     1.9  
    1.10  fun print_theorems_theory verbose = Toplevel.keep (fn state =>
    1.11    Toplevel.theory_of state |>
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 15 08:31:33 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 15 10:14:42 2014 +0100
     2.3 @@ -877,7 +877,7 @@
     2.4  val _ =
     2.5    Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
     2.6      (Scan.succeed (Toplevel.unknown_context o
     2.7 -      Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
     2.8 +      Toplevel.keep (Proof_Context.print_local_facts o Toplevel.context_of)));
     2.9  
    2.10  val _ =
    2.11    Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
     3.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 15 08:31:33 2014 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 15 10:14:42 2014 +0100
     3.3 @@ -162,7 +162,7 @@
     3.4    val print_syntax: Proof.context -> unit
     3.5    val print_abbrevs: Proof.context -> unit
     3.6    val print_binds: Proof.context -> unit
     3.7 -  val print_lthms: Proof.context -> unit
     3.8 +  val print_local_facts: Proof.context -> unit
     3.9    val print_cases: Proof.context -> unit
    3.10    val debug: bool Config.T
    3.11    val verbose: bool Config.T
    3.12 @@ -1267,21 +1267,23 @@
    3.13  val print_binds = Pretty.writeln o Pretty.chunks o pretty_binds;
    3.14  
    3.15  
    3.16 -(* local theorems *)
    3.17 +(* local facts *)
    3.18  
    3.19 -fun pretty_lthms ctxt =
    3.20 +fun pretty_local_facts ctxt =
    3.21    let
    3.22 -    val local_facts = facts_of ctxt;
    3.23 -    val props = Facts.props local_facts;
    3.24 -    val facts =
    3.25 +    val facts = facts_of ctxt;
    3.26 +    val props = Facts.props facts;
    3.27 +    val local_facts =
    3.28        (if null props then [] else [("<unnamed>", props)]) @
    3.29 -      Facts.dest_static [] local_facts;
    3.30 +      Facts.dest_static [Global_Theory.facts_of (theory_of ctxt)] facts;
    3.31    in
    3.32 -    if null facts then []
    3.33 -    else [Pretty.big_list "facts:" (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) facts)))]
    3.34 +    if null local_facts then []
    3.35 +    else
    3.36 +      [Pretty.big_list "local facts:"
    3.37 +        (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
    3.38    end;
    3.39  
    3.40 -val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;
    3.41 +val print_local_facts = Pretty.writeln o Pretty.chunks o pretty_local_facts;
    3.42  
    3.43  
    3.44  (* local contexts *)
    3.45 @@ -1405,7 +1407,7 @@
    3.46      pretty_ctxt ctxt @
    3.47      verb (pretty_abbrevs false) (K ctxt) @
    3.48      verb pretty_binds (K ctxt) @
    3.49 -    verb pretty_lthms (K ctxt) @
    3.50 +    verb pretty_local_facts (K ctxt) @
    3.51      verb pretty_cases (K ctxt) @
    3.52      verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
    3.53      verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))