1.1 --- a/src/Pure/pure_thy.ML	Sat Mar 15 22:07:32 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Sat Mar 15 22:07:34 2008 +0100
     1.3 @@ -250,25 +250,47 @@
     1.4  
     1.5  (* lookup/get thms *)
     1.6  
     1.7 -fun lookup_thms thy =
     1.8 +local
     1.9 +
    1.10 +fun lookup_thms thy xname =
    1.11    let
    1.12      val (space, thms) = #theorems (get_theorems thy);
    1.13 -    val thy_ref = Theory.check_thy thy;
    1.14 -  in
    1.15 -    fn name =>
    1.16 -      Option.map (map (Thm.transfer (Theory.deref thy_ref)))     (*dynamic identity*)
    1.17 -      (Symtab.lookup thms (NameSpace.intern space name)) (*static content*)
    1.18 -  end;
    1.19 +    val name = NameSpace.intern space xname;
    1.20 +  in Option.map (pair name) (Symtab.lookup thms name) end;
    1.21 +
    1.22 +fun lookup_fact thy xname =
    1.23 +  let
    1.24 +    val facts = all_facts_of thy;
    1.25 +    val name = NameSpace.intern (Facts.space_of facts) xname;
    1.26 +  in Option.map (pair name) (Facts.lookup facts name) end;
    1.27 +
    1.28 +fun show_result NONE = "none"
    1.29 +  | show_result (SOME (name, _)) = quote name;
    1.30 +
    1.31 +in
    1.32  
    1.33  fun get_thms theory thmref =
    1.34 -  let val name = name_of_thmref thmref in
    1.35 -    get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
    1.36 -    |> the_thms name |> select_thm thmref |> map (Thm.transfer theory)
    1.37 -  end;
    1.38 +  let
    1.39 +    val name = name_of_thmref thmref;
    1.40 +    val new_res = lookup_fact theory name;
    1.41 +    val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
    1.42 +    val is_same =
    1.43 +      (case (new_res, old_res) of
    1.44 +        (NONE, NONE) => true
    1.45 +      | (SOME (name1, ths1), SOME (name2, ths2)) => name1 = name2 andalso Thm.eq_thms (ths1, ths2)
    1.46 +      | _ => false);
    1.47 +    val _ =
    1.48 +      if is_same then ()
    1.49 +      else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
    1.50 +        show_result new_res ^ " vs " ^ show_result old_res ^
    1.51 +        Position.str_of (Position.thread_data ()));
    1.52 +  in Option.map #2 old_res |> the_thms name |> select_thm thmref |> map (Thm.transfer theory) end;
    1.53  
    1.54  fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
    1.55  fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
    1.56  
    1.57 +end;
    1.58 +
    1.59  
    1.60  (* thms_of etc. *)
    1.61