src/Pure/Isar/proof_context.ML
changeset 26687 fda7b0aff798
parent 26673 cda3df424bad
child 26695 65106c87b688
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 16 17:40:42 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 16 17:40:43 2008 +0200
     1.3 @@ -95,7 +95,6 @@
     1.4    val get_fact_single: Proof.context -> Facts.ref -> thm
     1.5    val get_thms: Proof.context -> xstring -> thm list
     1.6    val get_thm: Proof.context -> xstring -> thm
     1.7 -  val valid_thms: Proof.context -> string * thm list -> bool
     1.8    val add_path: string -> Proof.context -> Proof.context
     1.9    val no_base_names: Proof.context -> Proof.context
    1.10    val qualified_names: Proof.context -> Proof.context
    1.11 @@ -793,14 +792,14 @@
    1.12  
    1.13  local
    1.14  
    1.15 -fun retrieve_thms _ pick ctxt (Facts.Fact s) =
    1.16 +fun retrieve_thms pick ctxt (Facts.Fact s) =
    1.17        let
    1.18          val prop = Syntax.read_prop (set_mode mode_default ctxt) s
    1.19            |> singleton (Variable.polymorphic ctxt);
    1.20          val th = Goal.prove ctxt [] [] prop (K (ALLGOALS (some_fact_tac ctxt)))
    1.21            handle ERROR msg => cat_error msg "Failed to retrieve literal fact.";
    1.22        in pick "" [th] end
    1.23 -  | retrieve_thms from_thy pick ctxt xthmref =
    1.24 +  | retrieve_thms pick ctxt xthmref =
    1.25        let
    1.26          val thy = theory_of ctxt;
    1.27          val local_facts = facts_of ctxt;
    1.28 @@ -811,29 +810,20 @@
    1.29            else
    1.30              (case Facts.lookup (Context.Proof ctxt) local_facts name of
    1.31                SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
    1.32 -            | NONE => from_thy thy xthmref);
    1.33 +            | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
    1.34        in pick name thms end;
    1.35  
    1.36  in
    1.37  
    1.38 -val get_fact = retrieve_thms PureThy.get_fact (K I);
    1.39 -val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
    1.40 +val get_fact = retrieve_thms (K I);
    1.41 +val get_fact_single = retrieve_thms Facts.the_single;
    1.42  
    1.43 -fun get_thms_silent ctxt = retrieve_thms PureThy.get_fact_silent (K I) ctxt o Facts.named;
    1.44  fun get_thms ctxt = get_fact ctxt o Facts.named;
    1.45  fun get_thm ctxt = get_fact_single ctxt o Facts.named;
    1.46  
    1.47  end;
    1.48  
    1.49  
    1.50 -(* valid_thms *)
    1.51 -
    1.52 -fun valid_thms ctxt (name, ths) =
    1.53 -  (case try (fn () => get_thms_silent ctxt name) () of
    1.54 -    NONE => false
    1.55 -  | SOME ths' => Thm.eq_thms (ths, ths'));
    1.56 -
    1.57 -
    1.58  (* name space operations *)
    1.59  
    1.60  val add_path        = map_naming o NameSpace.add_path;
    1.61 @@ -1041,7 +1031,6 @@
    1.62    in
    1.63      ctxt2
    1.64      |> auto_bind_facts (flat propss)
    1.65 -    |> put_thms false (AutoBind.premsN, SOME (Assumption.prems_of ctxt2))
    1.66      |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
    1.67    end;
    1.68