# HG changeset patch
# User wenzelm
# Date 1394874882 -3600
# Node ID 1b9c089ed12de257af56378edc577b27a6fb4089
# Parent  f0a927235162c77db3f8634a9d7078434cdcceff
clarified print_local_facts;

diff -r f0a927235162 -r 1b9c089ed12d src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 08:31:33 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 10:14:42 2014 +0100
@@ -256,7 +256,7 @@
 (* print theorems *)
 
 val print_theorems_proof =
-  Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);
+  Toplevel.keep (Proof_Context.print_local_facts o Proof.context_of o Toplevel.proof_of);
 
 fun print_theorems_theory verbose = Toplevel.keep (fn state =>
   Toplevel.theory_of state |>
diff -r f0a927235162 -r 1b9c089ed12d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 15 08:31:33 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 15 10:14:42 2014 +0100
@@ -877,7 +877,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
     (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
+      Toplevel.keep (Proof_Context.print_local_facts o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
diff -r f0a927235162 -r 1b9c089ed12d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 15 08:31:33 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 15 10:14:42 2014 +0100
@@ -162,7 +162,7 @@
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
-  val print_lthms: Proof.context -> unit
+  val print_local_facts: Proof.context -> unit
   val print_cases: Proof.context -> unit
   val debug: bool Config.T
   val verbose: bool Config.T
@@ -1267,21 +1267,23 @@
 val print_binds = Pretty.writeln o Pretty.chunks o pretty_binds;
 
 
-(* local theorems *)
+(* local facts *)
 
-fun pretty_lthms ctxt =
+fun pretty_local_facts ctxt =
   let
-    val local_facts = facts_of ctxt;
-    val props = Facts.props local_facts;
-    val facts =
+    val facts = facts_of ctxt;
+    val props = Facts.props facts;
+    val local_facts =
       (if null props then [] else [("<unnamed>", props)]) @
-      Facts.dest_static [] local_facts;
+      Facts.dest_static [Global_Theory.facts_of (theory_of ctxt)] facts;
   in
-    if null facts then []
-    else [Pretty.big_list "facts:" (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) facts)))]
+    if null local_facts then []
+    else
+      [Pretty.big_list "local facts:"
+        (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
   end;
 
-val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;
+val print_local_facts = Pretty.writeln o Pretty.chunks o pretty_local_facts;
 
 
 (* local contexts *)
@@ -1405,7 +1407,7 @@
     pretty_ctxt ctxt @
     verb (pretty_abbrevs false) (K ctxt) @
     verb pretty_binds (K ctxt) @
-    verb pretty_lthms (K ctxt) @
+    verb pretty_local_facts (K ctxt) @
     verb pretty_cases (K ctxt) @
     verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))