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;