src/Pure/Tools/find_theorems.ML
 changeset 42360 da8817d01e7c parent 42358 b47d41d9f4b5 child 42669 04dfffda5671
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Apr 16 15:25:25 2011 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 16 15:47:52 2011 +0200
1.3 @@ -43,15 +43,15 @@
1.4
1.5  fun parse_pattern ctxt nm =
1.6    let
1.7 -    val consts = ProofContext.consts_of ctxt;
1.8 +    val consts = Proof_Context.consts_of ctxt;
1.9      val nm' =
1.10        (case Syntax.parse_term ctxt nm of
1.11          Const (c, _) => c
1.12        | _ => Consts.intern consts nm);
1.13    in
1.14      (case try (Consts.the_abbreviation consts) nm' of
1.15 -      SOME (_, rhs) => apply_dummies (ProofContext.expand_abbrevs ctxt rhs)
1.16 -    | NONE => ProofContext.read_term_pattern ctxt nm)
1.17 +      SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs)
1.18 +    | NONE => Proof_Context.read_term_pattern ctxt nm)
1.19    end;
1.20
1.21  fun read_criterion _ (Name name) = Name name
1.22 @@ -60,7 +60,7 @@
1.23    | read_criterion _ Elim = Elim
1.24    | read_criterion _ Dest = Dest
1.25    | read_criterion _ Solves = Solves
1.26 -  | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str)
1.27 +  | read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str)
1.28    | read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str);
1.29
1.30  fun pretty_criterion ctxt (b, c) =
1.31 @@ -131,7 +131,7 @@
1.32    returns: smallest substitution size*)
1.33  fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
1.34    let
1.35 -    val thy = ProofContext.theory_of ctxt;
1.36 +    val thy = Proof_Context.theory_of ctxt;
1.37
1.38      fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
1.39      fun matches pat =
1.40 @@ -216,7 +216,7 @@
1.41      in
1.42        (*elim rules always have assumptions, so an elim with one
1.43          assumption is as good as an intro rule with none*)
1.44 -      if is_nontrivial (ProofContext.theory_of ctxt) (major_prem_of theorem)
1.45 +      if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem)
1.46          andalso not (null successful)
1.47        then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
1.48      end
1.49 @@ -274,7 +274,7 @@
1.50      fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
1.51        | check (theorem, c as SOME thm_consts) =
1.52           (if subset (op =) (pat_consts, thm_consts) andalso
1.53 -            Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, prop_of theorem)
1.54 +            Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
1.55            then SOME (0, 0) else NONE, c);
1.56    in check end;
1.57
1.58 @@ -378,7 +378,7 @@
1.59  fun nicer_shortest ctxt =
1.60    let
1.61      (* FIXME global name space!? *)
1.62 -    val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
1.63 +    val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
1.64
1.65      val shorten =
1.66        Name_Space.extern
1.67 @@ -412,10 +412,10 @@
1.68        |> filter_out (Facts.is_concealed facts o #1);
1.69    in
1.70      maps Facts.selections
1.71 -     (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
1.72 +     (visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @
1.73
1.74
1.75 -      visible_facts (ProofContext.facts_of ctxt))
1.76 +      visible_facts (Proof_Context.facts_of ctxt))
1.77    end;
1.78
1.79  val limit = Unsynchronized.ref 40;
1.80 @@ -423,7 +423,7 @@
1.81  fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
1.82    let
1.83      val assms =
1.84 -      ProofContext.get_fact ctxt (Facts.named "local.assms")
1.85 +      Proof_Context.get_fact ctxt (Facts.named "local.assms")
1.86          handle ERROR _ => [];
1.87      val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
1.88      val opt_goal' = Option.map add_prems opt_goal;
```