Facts.extern_static;
authorwenzelm
Wed Apr 16 21:53:03 2008 +0200 (2008-04-16 ago)
changeset 2669565106c87b688
parent 26694 29f5c1a296bc
child 26696 1cd71fb32831
Facts.extern_static;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 16 21:53:02 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 16 21:53:03 2008 +0200
     1.3 @@ -1156,7 +1156,7 @@
     1.4      val local_facts = facts_of ctxt;
     1.5      val props = Facts.props local_facts;
     1.6      val facts =
     1.7 -      (if null props then [] else [("unnamed", props)]) @ Facts.extern_table local_facts;
     1.8 +      (if null props then [] else [("unnamed", props)]) @ Facts.extern_static local_facts;
     1.9    in
    1.10      if null facts andalso not (! verbose) then []
    1.11      else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]