src/Pure/Isar/proof_context.ML
changeset 26336 a0e2b706ce73
parent 26321 d875e70a94de
child 26346 17debd2fff8e
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -91,8 +91,8 @@
     1.4      -> Proof.context * (term list list * (Proof.context -> Proof.context))
     1.5    val fact_tac: thm list -> int -> tactic
     1.6    val some_fact_tac: Proof.context -> int -> tactic
     1.7 -  val get_thm: Proof.context -> thmref -> thm
     1.8 -  val get_thms: Proof.context -> thmref -> thm list
     1.9 +  val get_thm: Proof.context -> Facts.ref -> thm
    1.10 +  val get_thms: Proof.context -> Facts.ref -> thm list
    1.11    val valid_thms: Proof.context -> string * thm list -> bool
    1.12    val add_path: string -> Proof.context -> Proof.context
    1.13    val no_base_names: Proof.context -> Proof.context
    1.14 @@ -102,7 +102,7 @@
    1.15    val reset_naming: Proof.context -> Proof.context
    1.16    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
    1.17    val note_thmss: string ->
    1.18 -    ((bstring * attribute list) * (thmref * attribute list) list) list ->
    1.19 +    ((bstring * attribute list) * (Facts.ref * attribute list) list) list ->
    1.20        Proof.context -> (bstring * thm list) list * Proof.context
    1.21    val note_thmss_i: string ->
    1.22      ((bstring * attribute list) * (thm list * attribute list) list) list ->
    1.23 @@ -790,7 +790,7 @@
    1.24  
    1.25  (* get_thm(s) *)
    1.26  
    1.27 -fun retrieve_thms _ pick ctxt (Fact s) =
    1.28 +fun retrieve_thms _ pick ctxt (Facts.Fact s) =
    1.29        let
    1.30          val prop = Syntax.read_prop (set_mode mode_default ctxt) s
    1.31            |> singleton (Variable.polymorphic ctxt);
    1.32 @@ -802,17 +802,17 @@
    1.33          val thy = theory_of ctxt;
    1.34          val local_facts = facts_of ctxt;
    1.35          val space = Facts.space_of local_facts;
    1.36 -        val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
    1.37 -        val name = PureThy.name_of_thmref thmref;
    1.38 +        val thmref = Facts.map_name_of_ref (NameSpace.intern space) xthmref;
    1.39 +        val name = Facts.name_of_ref thmref;
    1.40          val thms =
    1.41            if name = "" then [Thm.transfer thy Drule.dummy_thm]
    1.42            else
    1.43              (case Facts.lookup local_facts name of
    1.44 -              SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
    1.45 +              SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
    1.46              | NONE => from_thy thy xthmref);
    1.47        in pick name thms end;
    1.48  
    1.49 -val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
    1.50 +val get_thm = retrieve_thms PureThy.get_thms Facts.the_single;
    1.51  val get_thms = retrieve_thms PureThy.get_thms (K I);
    1.52  val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
    1.53  
    1.54 @@ -820,7 +820,7 @@
    1.55  (* valid_thms *)
    1.56  
    1.57  fun valid_thms ctxt (name, ths) =
    1.58 -  (case try (fn () => get_thms_silent ctxt (Name name)) () of
    1.59 +  (case try (fn () => get_thms_silent ctxt (Facts.Named (name, NONE))) () of
    1.60      NONE => false
    1.61    | SOME ths' => Thm.eq_thms (ths, ths'));
    1.62