src/Pure/Isar/proof_context.ML
changeset 26673 cda3df424bad
parent 26463 9283b4185fdf
child 26687 fda7b0aff798
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 15 18:49:27 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 15 18:49:28 2008 +0200
     1.3 @@ -804,8 +804,7 @@
     1.4        let
     1.5          val thy = theory_of ctxt;
     1.6          val local_facts = facts_of ctxt;
     1.7 -        val space = Facts.space_of local_facts;
     1.8 -        val thmref = Facts.map_name_of_ref (NameSpace.intern space) xthmref;
     1.9 +        val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
    1.10          val name = Facts.name_of_ref thmref;
    1.11          val thms =
    1.12            if name = "" then [Thm.transfer thy Drule.dummy_thm]
    1.13 @@ -1167,7 +1166,8 @@
    1.14    let
    1.15      val local_facts = facts_of ctxt;
    1.16      val props = Facts.props local_facts;
    1.17 -    val facts = (if null props then I else cons ("unnamed", props)) (Facts.extern local_facts);
    1.18 +    val facts =
    1.19 +      (if null props then [] else [("unnamed", props)]) @ Facts.extern_table local_facts;
    1.20    in
    1.21      if null facts andalso not (! verbose) then []
    1.22      else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]