src/Pure/Isar/proof_context.ML
changeset 26695 65106c87b688
parent 26687 fda7b0aff798
child 26705 334d3fa649ea
     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)]